begin
reconsider u = one as Element of REAL+ by ARYTM_2:20;
Lm1:
for x, y, z being Element of REAL+ st x *' y = x *' z & x <> {} holds
y = z
Lm2:
for x, y, z being Element of REAL+ st x *' y <=' x *' z & x <> {} holds
y <=' z
Lm3:
for x being Element of REAL+ holds x -' x = {}
Lm4:
for x, y being Element of REAL+ st x = {} holds
y -' x = y
Lm5:
for x, y being Element of REAL+ holds (x + y) -' y = x
Lm6:
for x, y being Element of REAL+ st x <=' y holds
y -' (y -' x) = x
Lm7:
for z, y, x being Element of REAL+ holds
( z -' y <=' x iff z <=' x + y )
Lm8:
for y, x, z being Element of REAL+ st y <=' x holds
( z + y <=' x iff z <=' x -' y )
Lm9:
for z, y, x being Element of REAL+ holds (z -' y) -' x = z -' (x + y)
Lm10:
for y, z, x being Element of REAL+ holds (y -' z) -' x = (y -' x) -' z
Lm11:
for y, z, x being Element of REAL+ st y <=' z holds
x -' (z -' y) = (x + y) -' z
Lm12:
for z, x, y being Element of REAL+ st z <=' x & y <=' z holds
x -' (z -' y) = (x -' z) + y
Lm13:
for x, z, y being Element of REAL+ st x <=' z & y <=' z holds
x -' (z -' y) = y -' (z -' x)
Lm14:
for x, y, z being Element of REAL+ holds x *' (y -' z) = (x *' y) -' (x *' z)