let
x
be
Complex
;
:: thesis:
( not
x
^2
=
1 or
x
=
1 or
x
=

1 )
assume
x
^2
=
1 ;
:: thesis:
(
x
=
1 or
x
=

1 )
then
(
x

1)
*
(
x
+
1
)
=
0
;
then
(
x

1
=
0
or
x
+
1
=
0
) ;
hence
(
x
=
1 or
x
=

1 ) ;
:: thesis:
verum