let
x
,
y
be
Real
;
:: thesis:
(
0
<=
x
&
x
<=
y
implies
x
^2
<=
y
^2
)
assume
that
A1
:
0
<=
x
and
A2
:
x
<=
y
;
:: thesis:
x
^2
<=
y
^2
A3
:
x
*
y
<=
y
*
y
by
A1
,
A2
,
XREAL_1:64
;
x
*
x
<=
x
*
y
by
A1
,
A2
,
XREAL_1:64
;
hence
x
^2
<=
y
^2
by
A3
,
XXREAL_0:2
;
:: thesis:
verum