take r = - 1; :: thesis: r is negative
1 + (- 1) = 0 ;
then consider x1, x2, y1, y2 being Element of REAL such that
Lm9: 1 = [*x1,x2*] and
Lm10: ( - 1 = [*y1,y2*] & 0 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by XCMPLX_0:def 4;
Lm11: x1 = 1 by Lm1, Lm9;
Lm12: ( y1 = - 1 & + (x1,y1) = 0 ) by Lm1, Lm10;
reconsider z = 0 as Element of REAL+ by ARYTM_2:20;
now :: thesis: not - 1 in REAL+
assume - 1 in REAL+ ; :: thesis: contradiction
then ex x9, y9 being Element of REAL+ st
( x1 = x9 & y1 = y9 & z = x9 + y9 ) by Lm11, Lm12, ARYTM_0:def 1, ARYTM_2:20;
hence contradiction by Lm11, ARYTM_2:5; :: thesis: verum
end;
hence 0 > r by Lm7, XXREAL_0:def 5; :: according to XXREAL_0:def 7 :: thesis: verum