begin
Lm1:
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
Lm2:
for a being real number
for x1, x2 being Element of REAL st a = [*x1,x2*] holds
( x2 = 0 & a = x1 )
Lm3:
for a9, b9 being Element of REAL
for a, b being real number st a9 = a & b9 = b holds
+ (a9,b9) = a + b
Lm4:
{} in {{}}
by TARSKI:def 1;
Lm5:
for a, b, c being real number st a <= b holds
a + c <= b + c
Lm6:
for a, b, c, d being real number st a <= b & c <= d holds
a + c <= b + d
Lm7:
for a, b, c being real number st a <= b holds
a - c <= b - c
Lm8:
for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d
Lm9:
for a, b being real number st 0 < a holds
b < b + a
Lm10:
for a, c, b being real number st a + c <= b + c holds
a <= b
Lm11:
for a9, b9 being Element of REAL
for a, b being real number st a9 = a & b9 = b holds
* (a9,b9) = a * b
reconsider o = 0 as Element of REAL+ by ARYTM_2:20;
Lm12:
for a, b, c being real number st a <= b & 0 <= c holds
a * c <= b * c
Lm13:
for c, a, b being real number st 0 < c & a < b holds
a * c < b * c
begin
Lm14:
for a, b being real number st a <= b holds
- b <= - a
Lm15:
for b, a being real number st - b <= - a holds
a <= b
begin
Lm16:
for a, b, c being real number st a + b <= c holds
a <= c - b
Lm17:
for a, b, c being real number st a <= b - c holds
a + c <= b
Lm18:
for a, b, c being real number st a <= b + c holds
a - b <= c
Lm19:
for a, b, c being real number st a - b <= c holds
a <= b + c
Lm20:
for a, b, c, d being real number st a + b <= c + d holds
a - c <= d - b
begin
begin
Lm21:
for a, b being real number st a < b holds
0 < b - a
Lm22:
for a, b being real number st a <= b holds
0 <= b - a
begin
begin
Lm23:
for a, b being real number st a < b holds
a - b < 0
begin
Lm24:
for c, a, b being real number st c < 0 & a < b holds
b * c < a * c
Lm25:
for c, b, a being real number st 0 <= c & b <= a holds
b / c <= a / c
Lm26:
for c, a, b being real number st 0 < c & a < b holds
a / c < b / c
Lm27:
for a being real number st 0 < a holds
a / 2 < a
begin
begin
begin
begin
Lm28:
for a, b, c being real number st a <= b & c <= 0 holds
b * c <= a * c
begin
begin
Lm29:
for c, a, b being real number st c < 0 & a < b holds
b / c < a / c
Lm30:
for c, b, a being real number st c <= 0 & b / c < a / c holds
a < b
begin
Lm31:
for b, a being real number st b < 0 & a < b holds
b " < a "
begin
Lm32:
for a, b being real number st 0 < a & a <= b holds
b " <= a "
Lm33:
for b, a being real number st b < 0 & a <= b holds
b " <= a "
begin
Lm34:
for a, b being real number st 0 < a & a < b holds
b " < a "
Lm35:
for b being real number
for a being non positive non negative real number holds 0 = a * b
;
begin
begin
begin
begin
begin
Lm36:
for a being real number st 1 < a holds
a " < 1
Lm37:
for a, b being real number st a <= b & 0 <= a holds
a / b <= 1
Lm38:
for b, a being real number st b <= a & 0 <= a holds
b / a <= 1
begin
begin
begin
begin
begin
begin
begin
begin