begin
Lm1:
for r, s being real number st ( ( r in REAL+ & s in REAL+ & ex x', y' being Element of REAL+ st
( r = x' & s = y' & x' <=' y' ) ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & ex x', y' being Element of REAL+ st
( r = [0 ,x'] & s = [0 ,y'] & y' <=' x' ) ) or ( s in REAL+ & r in [:{0 },REAL+ :] ) ) holds
r <= s
Lm2:
for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
Lm3:
for x', y' being Element of REAL
for x, y being real number st x' = x & y' = y holds
+ x',y' = x + y
Lm4:
{} in {{} }
by TARSKI:def 1;
reconsider o = 0 as Element of REAL+ by ARYTM_2:21;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem