let
x
,
y
be
ExtReal
;
:: thesis:
(
min
(
x
,
y
)
)
+
(
max
(
x
,
y
)
)
=
x
+
y
per
cases
(
x
<=
y
or not
x
<=
y
)
;
suppose
A1
:
x
<=
y
;
:: thesis:
(
min
(
x
,
y
)
)
+
(
max
(
x
,
y
)
)
=
x
+
y
then
min
(
x
,
y
)
=
x
by
XXREAL_0:def 9
;
hence
(
min
(
x
,
y
))
+
(
max
(
x
,
y
)
)
=
x
+
y
by
A1
,
XXREAL_0:def 10
;
:: thesis:
verum
end;
suppose
A2
: not
x
<=
y
;
:: thesis:
(
min
(
x
,
y
)
)
+
(
max
(
x
,
y
)
)
=
x
+
y
then
min
(
x
,
y
)
=
y
by
XXREAL_0:def 9
;
hence
(
min
(
x
,
y
))
+
(
max
(
x
,
y
)
)
=
x
+
y
by
A2
,
XXREAL_0:def 10
;
:: thesis:
verum
end;
end;