begin
Lm1:
for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
begin
Lm2:
for r, s being real number st ( ( r in REAL+ & s in REAL+ & ex x9, y9 being Element of REAL+ st
( r = x9 & s = y9 & x9 <=' y9 ) ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( r = [0,x9] & s = [0,y9] & y9 <=' x9 ) ) or ( s in REAL+ & r in [:{0},REAL+:] ) ) holds
r <= s
Lm3:
{} in {{}}
by TARSKI:def 1;
Lm4:
for r, s being real number st r <= s & s <= r holds
r = s
Lm5:
for r, s, t being real number st r <= s holds
r + t <= s + t
Lm6:
for r, s, t being real number st r <= s & s <= t holds
r <= t
reconsider z = 0 as Element of REAL+ by ARYTM_2:20;
Lm7:
not 0 in [:{0},REAL+:]
by ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3;
reconsider j = 1 as Element of REAL+ by ARYTM_2:20;
z <=' j
by ARYTM_1:6;
then Lm8:
0 <= 1
by Lm2;
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;
Lm14:
for r, s being real number st r >= 0 & s > 0 holds
r + s > 0
Lm15:
for r, s being real number st r <= 0 & s < 0 holds
r + s < 0
reconsider o = 0 as Element of REAL+ by ARYTM_2:20;
Lm16:
for r, s, t being real number st r <= s & 0 <= t holds
r * t <= s * t
Lm17:
for r, s being real number st r > 0 & s > 0 holds
r * s > 0
Lm18:
for r, s being real number st r > 0 & s < 0 holds
r * s < 0
Lm19:
for s, t being real number st s <= t holds
- t <= - s
Lm20:
for r, s being real number st r <= 0 & s >= 0 holds
r * s <= 0
begin