1 / r <> 1
proof
assume 1 / r = 1 ; :: thesis: contradiction
then r * (1 / r) = r ;
hence contradiction by Def01, XCMPLX_1:106; :: thesis: verum
end;
hence 1 / r is non zero non unit Real by Def01; :: thesis: verum