A1: (r " ) " >= 0 by XXREAL_0:def 7;
assume A2: r " < 0 ; :: according to XXREAL_0:def 7 :: thesis: contradiction

per cases ( (r " ) " = 0 or (r " ) " > 0 ) by A1, Lm4;

suppose (r " ) " = 0 ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

suppose A3: (r " ) " > 0 ; :: thesis: contradiction

(r " ) * ((r " ) " ) = 1 by A2, XCMPLX_0:def 7;
hence contradiction by A2, A3, Lm8, Lm22; :: thesis: verum

end;

end;