let
x
,
y
be
Real
;
:: thesis:
(
0
<=
x
&
0
<=
y
&
x
^2
=
y
^2
implies
x
=
y
)
assume
that
A1
:
0
<=
x
and
A2
:
0
<=
y
;
:: thesis:
( not
x
^2
=
y
^2
or
x
=
y
)
assume
A3
:
x
^2
=
y
^2
;
:: thesis:
x
=
y
then
A4
:
y
<=
x
by
A1
,
Th16
;
x
<=
y
by
A2
,
A3
,
Th16
;
hence
x
=
y
by
A4
,
XXREAL_0:1
;
:: thesis:
verum