let
a
,
b
be
Real
;
:: thesis:
(

a
<=
b
&
b
<=
a
implies
b
^2
<=
a
^2
)
assume
that
A1
:

a
<=
b
and
A2
:
b
<=
a
;
:: thesis:
b
^2
<=
a
^2
per
cases
(
b
>=
0
or
b
<
0
)
;
suppose
b
>=
0
;
:: thesis:
b
^2
<=
a
^2
hence
b
^2
<=
a
^2
by
A2
,
Th15
;
:: thesis:
verum
end;
suppose
A3
:
b
<
0
;
:: thesis:
b
^2
<=
a
^2

(

a
)
>=

b
by
A1
,
XREAL_1:24
;
then
(

b
)
^2
<=
a
^2
by
A3
,
Th15
;
hence
b
^2
<=
a
^2
;
:: thesis:
verum
end;
end;