let a be complex number ; :: thesis: ( a <> 0 & a = 1 / a & not a = 1 implies a = - 1 )
assume a <> 0 ; :: thesis: ( not a = 1 / a or a = 1 or a = - 1 )
then ( not a = a " or a = 1 or a = - 1 ) by Lm19;
hence ( not a = 1 / a or a = 1 or a = - 1 ) by Lm4; :: thesis: verum