let
a
be
Real
;
:: thesis:
(
a
^2
<=
1 implies (

1
<=
a
&
a
<=
1 ) )
assume
a
^2
<=
1 ;
:: thesis:
(

1
<=
a
&
a
<=
1 )
then
(
a
^2
)

(
1
^2
)
<=
(
1
^2
)

(
1
^2
)
by
XREAL_1:9
;
then
(
a

1)
*
(
a
+
1
)
<=
0
;
hence
(

1
<=
a
&
a
<=
1 )
by
XREAL_1:93
;
:: thesis:
verum