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;

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+

hence
0 > r
by Lm7, XXREAL_0:def 5; :: according to XXREAL_0:def 7 :: thesis: verumassume
- 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;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