A1: (r " ) " > 0 by XXREAL_0:def 6;
assume A2: r " <= 0 ; :: according to XXREAL_0:def 6 :: thesis: contradiction
X: (r " ) * ((r " ) " ) = 1 by XCMPLX_0:def 7;
(r " ) * ((r " ) " ) <= 0 by A2, A1, Lm24;
hence contradiction by Lm8, X, Lm4; :: thesis: verum