let
a
be
Real
;
:: thesis:
(
0
<
a
&
a
<
1 implies
a
^2
<
a
)
assume
that
A1
:
0
<
a
and
A2
:
a
<
1 ;
:: thesis:
a
^2
<
a
a
*
a
<
a
*
1
by
A1
,
A2
,
XREAL_1:68
;
hence
a
^2
<
a
;
:: thesis:
verum