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