let
x
be
Real
;
:: thesis:
(
0
<=
x
&
x
<=
1 implies
x
^2
<=
x
)
assume
that
A1
:
0
<=
x
and
A2
:
x
<=
1 ;
:: thesis:
x
^2
<=
x
per
cases
(
0
=
x
or
0
<
x
)
by
A1
;
suppose
0
=
x
;
:: thesis:
x
^2
<=
x
hence
x
^2
<=
x
;
:: thesis:
verum
end;
suppose
A3
:
0
<
x
;
:: thesis:
x
^2
<=
x
per
cases
(
x
=
1 or
x
<
1 )
by
A2
,
XXREAL_0:1
;
suppose
x
=
1 ;
:: thesis:
x
^2
<=
x
hence
x
^2
<=
x
;
:: thesis:
verum
end;
suppose
x
<
1 ;
:: thesis:
x
^2
<=
x
hence
x
^2
<=
x
by
A3
,
Th13
;
:: thesis:
verum
end;
end;
end;
end;