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, Lm18; :: thesis: verum

end;

end;