let
m
,
n
be
Element
of
NAT
;
:: thesis:
(
m
^2
=
n
^2
implies
m
=
n
)
assume
A1
:
m
^2
=
n
^2
;
:: thesis:
m
=
n
per
cases
(
m
=
n
or
m
=

n
)
by
A1
,
SQUARE_1:40
;
suppose
m
=
n
;
:: thesis:
m
=
n
hence
m
=
n
;
:: thesis:
verum
end;
suppose
A2
:
m
=

n
;
:: thesis:
m
=
n
then
m
=

0
;
hence
m
=
n
by
A2
;
:: thesis:
verum
end;
end;