let
a
,
b
be
Complex
;
:: thesis:
( not
a
^2
=
b
^2
or
a
=
b
or
a
=

b
)
assume
a
^2
=
b
^2
;
:: thesis:
(
a
=
b
or
a
=

b
)
then
(
a
+
b
)
*
(
a

b
)
=
0
;
then
(
a
+
b
=
0
or
a

b
=
0
)
by
XCMPLX_1:6
;
hence
(
a
=
b
or
a
=

b
) ;
:: thesis:
verum