let a be Complex; :: 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 Lm18;
hence ( not a = 1 / a or a = 1 or a = - 1 ) by Lm4; :: thesis: verum