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