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