let
a
be
Real
;
:: thesis:
(

1
>=
a
implies

a
<=
a
^2
)
assume

1
>=
a
;
:: thesis:

a
<=
a
^2
then

(

1
)
<=

a
by
XREAL_1:24
;
then

a
<=
(

a
)
^2
by
XREAL_1:151
;
hence

a
<=
a
^2
;
:: thesis:
verum