let
r
be
Real
;
:: thesis:
( not
r
*
r
=
r
or
r
=
0
or
r
=
1 )
assume
r
*
r
=
r
;
:: thesis:
(
r
=
0
or
r
=
1 )
then
r
*
(
r

1
)
=
0
;
then
(
r
=
0
or
r

1
=
0
)
by
XCMPLX_1:6
;
hence
(
r
=
0
or
r
=
1 ) ;
:: thesis:
verum