:: ARYTM_1 semantic presentation

begin


theorem Th1: :: ARYTM_1:1
for x, y being Element of REAL+ st x + y = y holds
x = {}
proof
let x, y be Element of REAL+ ; ::_thesis: ( x + y = y implies x = {} )
reconsider o = {} as Element of REAL+ by ARYTM_2:20;
assume  x + y = y ; ::_thesis: x = {}
then  x + y = y + o by ARYTM_2:def_8;
hence  x = {} by ARYTM_2:11; ::_thesis: verum
end;

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
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x *' y = x *' z & x <> {} implies y = z )
assume A1: x *' y = x *' z ; ::_thesis: ( not x <> {} or y = z )
assume  x <> {} ; ::_thesis: y = z
then consider x1 being Element of REAL+  such that
A2: x *' x1 = one by ARYTM_2:14;
thus y = (x *' x1) *' y by A2, ARYTM_2:15
.= x1 *' (x *' z) by A1, ARYTM_2:12
.= (x *' x1) *' z by ARYTM_2:12
.= z by A2, ARYTM_2:15 ; ::_thesis: verum
end;

theorem :: ARYTM_1:2
for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )
proof
let x, y be Element of REAL+ ; ::_thesis: ( not x *' y = {} or x = {} or y = {} )
assume A1: x *' y = {} ; ::_thesis: ( x = {} or y = {} )
assume  x <> {} ; ::_thesis: y = {}
then consider x1 being Element of REAL+  such that
A2: x *' x1 = one by ARYTM_2:14;
thus y = (x *' x1) *' y by A2, ARYTM_2:15
.= (x *' y) *' x1 by ARYTM_2:12
.= {} by A1, ARYTM_2:4 ; ::_thesis: verum
end;

theorem Th3: :: ARYTM_1:3
for x, y, z being Element of REAL+ st x <=' y & y <=' z holds
x <=' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' z implies x <=' z )
assume  x <=' y ; ::_thesis: ( not y <=' z or x <=' z )
then consider z1 being Element of REAL+  such that
A1: x + z1 = y by ARYTM_2:9;
assume  y <=' z ; ::_thesis: x <=' z
then consider z2 being Element of REAL+  such that
A2: y + z2 = z by ARYTM_2:9;
 z = x + (z1 + z2) by A1, A2, ARYTM_2:6;
hence  x <=' z by ARYTM_2:19; ::_thesis: verum
end;

theorem Th4: :: ARYTM_1:4
for x, y being Element of REAL+ st x <=' y & y <=' x holds
x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y <=' x implies x = y )
assume  x <=' y ; ::_thesis: ( not y <=' x or x = y )
then consider z1 being Element of REAL+  such that
A1: x + z1 = y by ARYTM_2:9;
assume  y <=' x ; ::_thesis: x = y
then consider z2 being Element of REAL+  such that
A2: y + z2 = x by ARYTM_2:9;
 x = x + (z1 + z2) by A1, A2, ARYTM_2:6;
then  z1 = {} by Th1, ARYTM_2:5;
hence  x = y by A1, ARYTM_2:def_8; ::_thesis: verum
end;

theorem Th5: :: ARYTM_1:5
for x, y being Element of REAL+ st x <=' y & y = {} holds
x = {}
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y = {} implies x = {} )
assume  x <=' y ; ::_thesis: ( not y = {} or x = {} )
then  ex z being Element of REAL+ st x + z = y by ARYTM_2:9;
hence  ( not y = {} or x = {} ) by ARYTM_2:5; ::_thesis: verum
end;

theorem Th6: :: ARYTM_1:6
for x, y being Element of REAL+ st x = {} holds
x <=' y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies x <=' y )
assume  x = {} ; ::_thesis: x <=' y
then  x + y = y by ARYTM_2:def_8;
hence  x <=' y by ARYTM_2:19; ::_thesis: verum
end;

theorem Th7: :: ARYTM_1:7
for x, y, z being Element of REAL+ holds
( x <=' y iff x + z <=' y + z )
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y iff x + z <=' y + z )
thus  ( x <=' y implies x + z <=' y + z ) ::_thesis: ( x + z <=' y + z implies x <=' y )
proof
assume  x <=' y ; ::_thesis: x + z <=' y + z
then consider z0 being Element of REAL+  such that
A1: x + z0 = y by ARYTM_2:9;
 (x + z) + z0 = y + z by A1, ARYTM_2:6;
hence  x + z <=' y + z by ARYTM_2:19; ::_thesis: verum
end;
assume  x + z <=' y + z ; ::_thesis: x <=' y
then consider z0 being Element of REAL+  such that
A2: (x + z) + z0 = y + z by ARYTM_2:9;
 y + z = (x + z0) + z by A2, ARYTM_2:6;
hence  x <=' y by ARYTM_2:11, ARYTM_2:19; ::_thesis: verum
end;

theorem Th8: :: ARYTM_1:8
for x, y, z being Element of REAL+ st x <=' y holds
x *' z <=' y *' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies x *' z <=' y *' z )
assume  x <=' y ; ::_thesis: x *' z <=' y *' z
then consider z0 being Element of REAL+  such that
A1: x + z0 = y by ARYTM_2:9;
 y *' z = (x *' z) + (z0 *' z) by A1, ARYTM_2:13;
hence  x *' z <=' y *' z by ARYTM_2:19; ::_thesis: verum
end;

Lm2:  for x, y, z being Element of REAL+ st x *' y <=' x *' z & x <> {} holds
y <=' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x *' y <=' x *' z & x <> {} implies y <=' z )
assume  x *' y <=' x *' z ; ::_thesis: ( not x <> {} or y <=' z )
then consider z0 being Element of REAL+  such that
A1: (x *' y) + z0 = x *' z by ARYTM_2:9;
assume A2: x <> {} ; ::_thesis: y <=' z
then consider x1 being Element of REAL+  such that
A3: x *' x1 = one by ARYTM_2:14;
x *' z = (x *' y) + (u *' z0) by A1, ARYTM_2:15
.= (x *' y) + (x *' (x1 *' z0)) by A3, ARYTM_2:12
.= x *' (y + (x1 *' z0)) by ARYTM_2:13 ;
hence  y <=' z by A2, Lm1, ARYTM_2:19; ::_thesis: verum
end;

definition
let x, y be Element of REAL+ ;
funcx -' y ->  Element of REAL+  means :Def1: :: ARYTM_1:def 1
it + y = x if y <=' x
otherwise it = {} ;
existence
 ( ( y <=' x implies ex b1 being Element of REAL+ st b1 + y = x ) & ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) )
proof
hereby  ::_thesis: ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} )
assume  y <=' x ; ::_thesis: ex IT being Element of REAL+ st IT + y = x
then  ex IT being Element of REAL+ st y + IT = x by ARYTM_2:9;
hence  ex IT being Element of REAL+ st IT + y = x ; ::_thesis: verum
end;
thus  ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) by ARYTM_2:20; ::_thesis: verum
end;
correctness
consistency
for b1 being Element of REAL+ holds verum;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( y <=' x & b1 + y = x & b2 + y = x implies b1 = b2 ) & ( not y <=' x & b1 = {} & b2 = {} implies b1 = b2 ) );
by ARYTM_2:11;
end;

:: deftheorem Def1 defines -' ARYTM_1:def_1_:_
 for x, y, b3 being Element of REAL+ holds
( ( y <=' x implies ( b3 = x -' y iff b3 + y = x ) ) & ( not y <=' x implies ( b3 = x -' y iff b3 = {} ) ) );

Lm3:  for x being Element of REAL+ holds x -' x = {}
proof
let x be Element of REAL+ ; ::_thesis: x -' x = {}
 x <=' x ;
then  (x -' x) + x = x by Def1;
hence  x -' x = {} by Th1; ::_thesis: verum
end;

theorem Th9: :: ARYTM_1:9
for x, y being Element of REAL+ holds
( x <=' y or x -' y <> {} )
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y or x -' y <> {} )
assume A1: not x <=' y ; ::_thesis: x -' y <> {}
assume A2: x -' y = {} ; ::_thesis: contradiction
 (x -' y) + y = x by A1, Def1;
then  x = y by A2, ARYTM_2:def_8;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: ARYTM_1:10
for x, y being Element of REAL+ st x <=' y & y -' x = {} holds
x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y & y -' x = {} implies x = y )
assume A1: x <=' y ; ::_thesis: ( not y -' x = {} or x = y )
assume  y -' x = {} ; ::_thesis: x = y
then  y <=' x by Th9;
hence  x = y by A1, Th4; ::_thesis: verum
end;

theorem Th11: :: ARYTM_1:11
for x, y being Element of REAL+ holds x -' y <=' x
proof
let x, y be Element of REAL+ ; ::_thesis: x -' y <=' x
percases ( y <=' x or not y <=' x ) ;
suppose y <=' x ; ::_thesis: x -' y <=' x
then  (x -' y) + y = x by Def1;
hence  x -' y <=' x by ARYTM_2:19; ::_thesis: verum
end;
suppose not y <=' x ; ::_thesis: x -' y <=' x
then  x -' y = {} by Def1;
hence  x -' y <=' x by Th6; ::_thesis: verum
end;
end;
end;

Lm4:  for x, y being Element of REAL+ st x = {} holds
y -' x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x = {} implies y -' x = y )
assume A1: x = {} ; ::_thesis: y -' x = y
then A2: x <=' y by Th6;
thus y -' x = (y -' x) + x by A1, ARYTM_2:def_8
.= y by A2, Def1 ; ::_thesis: verum
end;

Lm5:  for x, y being Element of REAL+ holds (x + y) -' y = x
proof
let x, y be Element of REAL+ ; ::_thesis: (x + y) -' y = x
 y <=' x + y by ARYTM_2:19;
hence  (x + y) -' y = x by Def1; ::_thesis: verum
end;

Lm6:  for x, y being Element of REAL+ st x <=' y holds
y -' (y -' x) = x
proof
let x, y be Element of REAL+ ; ::_thesis: ( x <=' y implies y -' (y -' x) = x )
assume A1: x <=' y ; ::_thesis: y -' (y -' x) = x
 y -' x <=' y by Th11;
then (y -' (y -' x)) + (y -' x) = y by Def1
.= (y -' x) + x by A1, Def1 ;
hence  y -' (y -' x) = x by ARYTM_2:11; ::_thesis: verum
end;

Lm7:  for z, y, x being Element of REAL+ holds
( z -' y <=' x iff z <=' x + y )
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( z -' y <=' x iff z <=' x + y )
percases ( y <=' z or not y <=' z ) ;
suppose y <=' z ; ::_thesis: ( z -' y <=' x iff z <=' x + y )
then  (z -' y) + y = z by Def1;
hence  ( z -' y <=' x iff z <=' x + y ) by Th7; ::_thesis: verum
end;
supposeA1: not y <=' z ; ::_thesis: ( z -' y <=' x iff z <=' x + y )
A2: y <=' x + y by ARYTM_2:19;
 z -' y = {} by A1, Def1;
hence  ( z -' y <=' x iff z <=' x + y ) by A1, A2, Th3, Th6; ::_thesis: verum
end;
end;
end;

Lm8:  for y, x, z being Element of REAL+ st y <=' x holds
( z + y <=' x iff z <=' x -' y )
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x implies ( z + y <=' x iff z <=' x -' y ) )
assume  y <=' x ; ::_thesis: ( z + y <=' x iff z <=' x -' y )
then  (x -' y) + y = x by Def1;
hence  ( z + y <=' x iff z <=' x -' y ) by Th7; ::_thesis: verum
end;

Lm9:  for z, y, x being Element of REAL+ holds (z -' y) -' x = z -' (x + y)
proof
let z, y, x be Element of REAL+ ; ::_thesis: (z -' y) -' x = z -' (x + y)
percases ( x + y <=' z or x = {} or ( not y <=' z & x <> {} ) or ( not x + y <=' z & y <=' z ) ) ;
supposeA1: x + y <=' z ; ::_thesis: (z -' y) -' x = z -' (x + y)
 y <=' x + y by ARYTM_2:19;
then A2: y <=' z by A1, Th3;
then A3: x <=' z -' y by A1, Lm8;
((z -' y) -' x) + (x + y) = (((z -' y) -' x) + x) + y by ARYTM_2:6
.= (z -' y) + y by A3, Def1
.= z by A2, Def1 ;
hence  (z -' y) -' x = z -' (x + y) by A1, Def1; ::_thesis: verum
end;
supposeA4: x = {} ; ::_thesis: (z -' y) -' x = z -' (x + y)
hence (z -' y) -' x = z -' y by Lm4
.= z -' (x + y) by A4, ARYTM_2:def_8 ;
::_thesis: verum
end;
supposethat A5: not y <=' z and
A6: x <> {} ; ::_thesis: (z -' y) -' x = z -' (x + y)
 y <=' y + x by ARYTM_2:19;
then A7: not x + y <=' z by A5, Th3;
now__::_thesis:_not_x_<='_z_-'_y
assume A8: x <=' z -' y ; ::_thesis: contradiction
 z -' y = {} by A5, Def1;
hence  contradiction by A6, A8, Th5; ::_thesis: verum
end;
hence (z -' y) -' x = {} by Def1
.= z -' (x + y) by A7, Def1 ;
::_thesis: verum
end;
supposethat A9: not x + y <=' z and
A10: y <=' z ; ::_thesis: (z -' y) -' x = z -' (x + y)
 not x <=' z -' y by A9, A10, Lm8;
hence (z -' y) -' x = {} by Def1
.= z -' (x + y) by A9, Def1 ;
::_thesis: verum
end;
end;
end;

Lm10:  for y, z, x being Element of REAL+ holds (y -' z) -' x = (y -' x) -' z
proof
let y, z, x be Element of REAL+ ; ::_thesis: (y -' z) -' x = (y -' x) -' z
thus (y -' z) -' x = y -' (x + z) by Lm9
.= (y -' x) -' z by Lm9 ; ::_thesis: verum
end;

theorem :: ARYTM_1:12
for y, x, z being Element of REAL+ st y <=' x & y <=' z holds
x + (z -' y) = (x -' y) + z
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & y <=' z implies x + (z -' y) = (x -' y) + z )
assume that
A1: y <=' x and
A2: y <=' z ; ::_thesis: x + (z -' y) = (x -' y) + z
(x + (z -' y)) + y = x + ((z -' y) + y) by ARYTM_2:6
.= x + z by A2, Def1
.= ((x -' y) + y) + z by A1, Def1
.= ((x -' y) + z) + y by ARYTM_2:6 ;
hence  x + (z -' y) = (x -' y) + z by ARYTM_2:11; ::_thesis: verum
end;

theorem Th13: :: ARYTM_1:13
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) -' z
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x + (y -' z) = (x + y) -' z )
assume A1: z <=' y ; ::_thesis: x + (y -' z) = (x + y) -' z
 y <=' x + y by ARYTM_2:19;
then A2: z <=' x + y by A1, Th3;
(x + (y -' z)) + z = x + ((y -' z) + z) by ARYTM_2:6
.= x + y by A1, Def1
.= ((x + y) -' z) + z by A2, Def1 ;
hence  x + (y -' z) = (x + y) -' z by ARYTM_2:11; ::_thesis: verum
end;

Lm11:  for y, z, x being Element of REAL+ st y <=' z holds
x -' (z -' y) = (x + y) -' z
proof
let y, z, x be Element of REAL+ ; ::_thesis: ( y <=' z implies x -' (z -' y) = (x + y) -' z )
assume A1: y <=' z ; ::_thesis: x -' (z -' y) = (x + y) -' z
percases ( z -' y <=' x or not z -' y <=' x ) ;
supposeA2: z -' y <=' x ; ::_thesis: x -' (z -' y) = (x + y) -' z
then A3: z <=' x + y by Lm7;
(x -' (z -' y)) + (z -' y) = x by A2, Def1
.= (x + z) -' z by Lm5
.= (x + (y + (z -' y))) -' z by A1, Def1
.= ((x + y) + (z -' y)) -' z by ARYTM_2:6
.= ((x + y) -' z) + (z -' y) by A3, Th13 ;
hence  x -' (z -' y) = (x + y) -' z by ARYTM_2:11; ::_thesis: verum
end;
supposeA4: not z -' y <=' x ; ::_thesis: x -' (z -' y) = (x + y) -' z
then A5: not z <=' x + y by Lm7;
thus x -' (z -' y) = {} by A4, Def1
.= (x + y) -' z by A5, Def1 ; ::_thesis: verum
end;
end;
end;

Lm12:  for z, x, y being Element of REAL+ st z <=' x & y <=' z holds
x -' (z -' y) = (x -' z) + y
proof
let z, x, y be Element of REAL+ ; ::_thesis: ( z <=' x & y <=' z implies x -' (z -' y) = (x -' z) + y )
assume that
A1: z <=' x and
A2: y <=' z ; ::_thesis: x -' (z -' y) = (x -' z) + y
thus x -' (z -' y) = (x + y) -' z by A2, Lm11
.= (x -' z) + y by A1, Th13 ; ::_thesis: verum
end;

Lm13:  for x, z, y being Element of REAL+ st x <=' z & y <=' z holds
x -' (z -' y) = y -' (z -' x)
proof
let x, z, y be Element of REAL+ ; ::_thesis: ( x <=' z & y <=' z implies x -' (z -' y) = y -' (z -' x) )
assume that
A1: x <=' z and
A2: y <=' z ; ::_thesis: x -' (z -' y) = y -' (z -' x)
thus x -' (z -' y) = (x + y) -' z by A2, Lm11
.= y -' (z -' x) by A1, Lm11 ; ::_thesis: verum
end;

theorem :: ARYTM_1:14
for z, x, y being Element of REAL+ st z <=' x & y <=' z holds
(x -' z) + y = x -' (z -' y)
proof
let z, x, y be Element of REAL+ ; ::_thesis: ( z <=' x & y <=' z implies (x -' z) + y = x -' (z -' y) )
assume that
A1: z <=' x and
A2: y <=' z ; ::_thesis: (x -' z) + y = x -' (z -' y)
thus x -' (z -' y) = (x + y) -' z by A2, Lm11
.= (x -' z) + y by A1, Th13 ; ::_thesis: verum
end;

theorem :: ARYTM_1:15
for y, x, z being Element of REAL+ st y <=' x & y <=' z holds
(z -' y) + x = (x -' y) + z
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & y <=' z implies (z -' y) + x = (x -' y) + z )
assume that
A1: y <=' x and
A2: y <=' z ; ::_thesis: (z -' y) + x = (x -' y) + z
((z -' y) + x) + y = ((z -' y) + y) + x by ARYTM_2:6
.= z + x by A2, Def1
.= ((x -' y) + y) + z by A1, Def1
.= ((x -' y) + z) + y by ARYTM_2:6 ;
hence  (z -' y) + x = (x -' y) + z by ARYTM_2:11; ::_thesis: verum
end;

theorem :: ARYTM_1:16
for x, y, z being Element of REAL+ st x <=' y holds
z -' y <=' z -' x
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies z -' y <=' z -' x )
assume A1: x <=' y ; ::_thesis: z -' y <=' z -' x
percases ( y <=' z or not y <=' z ) ;
supposeA2: y <=' z ; ::_thesis: z -' y <=' z -' x
 (z -' y) + x <=' (z -' y) + y by A1, Th7;
then A3: (z -' y) + x <=' z by A2, Def1;
 x <=' z by A1, A2, Th3;
then  (z -' y) + x <=' (z -' x) + x by A3, Def1;
hence  z -' y <=' z -' x by Th7; ::_thesis: verum
end;
suppose not y <=' z ; ::_thesis: z -' y <=' z -' x
then  z -' y = {} by Def1;
hence  z -' y <=' z -' x by Th6; ::_thesis: verum
end;
end;
end;

theorem :: ARYTM_1:17
for x, y, z being Element of REAL+ st x <=' y holds
x -' z <=' y -' z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y implies x -' z <=' y -' z )
assume A1: x <=' y ; ::_thesis: x -' z <=' y -' z
percases ( z <=' x or not z <=' x ) ;
supposeA2: z <=' x ; ::_thesis: x -' z <=' y -' z
then  z <=' y by A1, Th3;
then A3: (y -' z) + z = y by Def1;
 (x -' z) + z = x by A2, Def1;
hence  x -' z <=' y -' z by A1, A3, Th7; ::_thesis: verum
end;
suppose not z <=' x ; ::_thesis: x -' z <=' y -' z
then  x -' z = {} by Def1;
hence  x -' z <=' y -' z by Th6; ::_thesis: verum
end;
end;
end;

Lm14:  for x, y, z being Element of REAL+ holds x *' (y -' z) = (x *' y) -' (x *' z)
proof
let x, y, z be Element of REAL+ ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z)
percases ( z <=' y or x = {} or ( not z <=' y & x <> {} ) ) ;
supposeA1: z <=' y ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z)
then A2: x *' z <=' x *' y by Th8;
(x *' (y -' z)) + (x *' z) = x *' ((y -' z) + z) by ARYTM_2:13
.= x *' y by A1, Def1
.= ((x *' y) -' (x *' z)) + (x *' z) by A2, Def1 ;
hence  x *' (y -' z) = (x *' y) -' (x *' z) by ARYTM_2:11; ::_thesis: verum
end;
supposeA3: x = {} ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z)
then  x *' y = {} by ARYTM_2:4;
hence x *' (y -' z) = x *' y by A3, ARYTM_2:4
.= (x *' y) -' (x *' z) by A3, Lm4, ARYTM_2:4 ;
::_thesis: verum
end;
supposeA4: ( not z <=' y & x <> {} ) ; ::_thesis: x *' (y -' z) = (x *' y) -' (x *' z)
then A5: not x *' z <=' x *' y by Lm2;
 y -' z = {} by A4, Def1;
hence x *' (y -' z) = {} by ARYTM_2:4
.= (x *' y) -' (x *' z) by A5, Def1 ;
::_thesis: verum
end;
end;
end;

definition
let x, y be Element of REAL+ ;
funcx - y ->  set  equals :Def2: :: ARYTM_1:def 2
x -' y if y <=' x
otherwise [{},(y -' x)];
correctness
coherence
( ( y <=' x implies x -' y is set ) & ( not y <=' x implies [{},(y -' x)] is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def2 defines - ARYTM_1:def_2_:_
 for x, y being Element of REAL+ holds
( ( y <=' x implies x - y = x -' y ) & ( not y <=' x implies x - y = [{},(y -' x)] ) );

theorem :: ARYTM_1:18
for x being Element of REAL+ holds x - x = {}
proof
let x be Element of REAL+ ; ::_thesis: x - x = {}
 x <=' x ;
then  x - x = x -' x by Def2;
hence  x - x = {} by Lm3; ::_thesis: verum
end;

theorem :: ARYTM_1:19
for x, y being Element of REAL+ st x = {} & y <> {} holds
x - y = [{},y]
proof
let x, y be Element of REAL+ ; ::_thesis: ( x = {} & y <> {} implies x - y = [{},y] )
assume that
A1: x = {} and
A2: y <> {} ; ::_thesis: x - y = [{},y]
 x <=' y by A1, Th6;
then  not y <=' x by A1, A2, Th4;
hence x - y = [{},(y -' x)] by Def2
.= [{},y] by A1, Lm4 ;
::_thesis: verum
end;

theorem :: ARYTM_1:20
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) - z
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x + (y -' z) = (x + y) - z )
assume A1: z <=' y ; ::_thesis: x + (y -' z) = (x + y) - z
 y <=' x + y by ARYTM_2:19;
then  z <=' x + y by A1, Th3;
then  (x + y) - z = (x + y) -' z by Def2;
hence  x + (y -' z) = (x + y) - z by A1, Th13; ::_thesis: verum
end;

theorem :: ARYTM_1:21
for z, y, x being Element of REAL+ st not z <=' y holds
x - (z -' y) = (x + y) - z
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( not z <=' y implies x - (z -' y) = (x + y) - z )
assume A1: not z <=' y ; ::_thesis: x - (z -' y) = (x + y) - z
percases ( z -' y <=' x or not z -' y <=' x ) ;
supposeA2: z -' y <=' x ; ::_thesis: x - (z -' y) = (x + y) - z
then  z <=' x + y by Lm7;
then A3: (x + y) - z = (x + y) -' z by Def2;
 x - (z -' y) = x -' (z -' y) by A2, Def2;
hence  x - (z -' y) = (x + y) - z by A1, A3, Lm11; ::_thesis: verum
end;
supposeA4: not z -' y <=' x ; ::_thesis: x - (z -' y) = (x + y) - z
then A5: not z <=' x + y by Lm7;
 (z -' y) -' x = z -' (x + y) by Lm9;
hence x - (z -' y) = [{},(z -' (x + y))] by A4, Def2
.= (x + y) - z by A5, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: ARYTM_1:22
for y, x, z being Element of REAL+ st y <=' x & not y <=' z holds
x - (y -' z) = (x -' y) + z
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x & not y <=' z implies x - (y -' z) = (x -' y) + z )
assume that
A1: y <=' x and
A2: not y <=' z ; ::_thesis: x - (y -' z) = (x -' y) + z
 y -' z <=' y by Th11;
then  y -' z <=' x by A1, Th3;
then  x - (y -' z) = x -' (y -' z) by Def2;
hence  x - (y -' z) = (x -' y) + z by A1, A2, Lm12; ::_thesis: verum
end;

theorem :: ARYTM_1:23
for y, x, z being Element of REAL+ st not y <=' x & not y <=' z holds
x - (y -' z) = z - (y -' x)
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( not y <=' x & not y <=' z implies x - (y -' z) = z - (y -' x) )
assume A1: ( not y <=' x & not y <=' z ) ; ::_thesis: x - (y -' z) = z - (y -' x)
percases ( y <=' x + z or not y <=' x + z ) ;
supposeA2: y <=' x + z ; ::_thesis: x - (y -' z) = z - (y -' x)
then  y -' x <=' z by Lm7;
then A3: z - (y -' x) = z -' (y -' x) by Def2;
 y -' z <=' x by A2, Lm7;
then  x - (y -' z) = x -' (y -' z) by Def2;
hence  x - (y -' z) = z - (y -' x) by A1, A3, Lm13; ::_thesis: verum
end;
supposeA4: not y <=' x + z ; ::_thesis: x - (y -' z) = z - (y -' x)
then A5: not y -' x <=' z by Lm7;
A6: (y -' z) -' x = (y -' x) -' z by Lm10;
 not y -' z <=' x by A4, Lm7;
hence x - (y -' z) = [{},((y -' x) -' z)] by A6, Def2
.= z - (y -' x) by A5, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: ARYTM_1:24
for y, x, z being Element of REAL+ st y <=' x holds
x - (y + z) = (x -' y) - z
proof
let y, x, z be Element of REAL+ ; ::_thesis: ( y <=' x implies x - (y + z) = (x -' y) - z )
assume A1: y <=' x ; ::_thesis: x - (y + z) = (x -' y) - z
percases ( y + z <=' x or ( not y + z <=' x & x <=' y ) or ( not y + z <=' x & not x <=' y ) ) ;
supposeA2: y + z <=' x ; ::_thesis: x - (y + z) = (x -' y) - z
then  z <=' x -' y by A1, Lm8;
then A3: (x -' y) - z = (x -' y) -' z by Def2;
 x - (y + z) = x -' (y + z) by A2, Def2;
hence  x - (y + z) = (x -' y) - z by A3, Lm9; ::_thesis: verum
end;
supposethat A4: not y + z <=' x and
A5: x <=' y ; ::_thesis: x - (y + z) = (x -' y) - z
A6: not z <=' x -' y by A1, A4, Lm8;
A7: (x + z) -' x = z by Lm5
.= z -' (x -' x) by Lm3, Lm4 ;
 x = y by A1, A5, Th4;
hence x - (y + z) = [{},(z -' (x -' y))] by A4, A7, Def2
.= (x -' y) - z by A6, Def2 ;
::_thesis: verum
end;
supposethat A8: not y + z <=' x and
A9: not x <=' y ; ::_thesis: x - (y + z) = (x -' y) - z
A10: not z <=' x -' y by A1, A8, Lm8;
 (y + z) -' x = z -' (x -' y) by A9, Lm11;
hence x - (y + z) = [{},(z -' (x -' y))] by A8, Def2
.= (x -' y) - z by A10, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: ARYTM_1:25
for x, y, z being Element of REAL+ st x <=' y & z <=' y holds
(y -' z) - x = (y -' x) - z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <=' y & z <=' y implies (y -' z) - x = (y -' x) - z )
assume that
A1: x <=' y and
A2: z <=' y ; ::_thesis: (y -' z) - x = (y -' x) - z
percases ( x + z <=' y or ( not x + z <=' y & y <=' x ) or ( not x + z <=' y & y <=' z ) or ( not x + z <=' y & not y <=' x & not y <=' z ) ) ;
supposeA3: x + z <=' y ; ::_thesis: (y -' z) - x = (y -' x) - z
then  z <=' y -' x by A1, Lm8;
then A4: (y -' x) -' z = (y -' x) - z by Def2;
 x <=' y -' z by A2, A3, Lm8;
then  (y -' z) -' x = (y -' z) - x by Def2;
hence  (y -' z) - x = (y -' x) - z by A4, Lm10; ::_thesis: verum
end;
supposethat A5: not x + z <=' y and
A6: y <=' x ; ::_thesis: (y -' z) - x = (y -' x) - z
A7: not x <=' y -' z by A2, A5, Lm8;
A8: not z <=' y -' x by A1, A5, Lm8;
A9: x = y by A1, A6, Th4;
then x -' (x -' z) = z by A2, Lm6
.= z -' (x -' x) by Lm3, Lm4 ;
hence (y -' z) - x = [{},(z -' (y -' x))] by A7, A9, Def2
.= (y -' x) - z by A8, Def2 ;
::_thesis: verum
end;
supposethat A10: not x + z <=' y and
A11: y <=' z ; ::_thesis: (y -' z) - x = (y -' x) - z
A12: not x <=' y -' z by A2, A10, Lm8;
A13: not z <=' y -' x by A1, A10, Lm8;
A14: z = y by A2, A11, Th4;
x -' (z -' z) = x by Lm3, Lm4
.= z -' (z -' x) by A1, A14, Lm6 ;
hence (y -' z) - x = [{},(z -' (y -' x))] by A12, A14, Def2
.= (y -' x) - z by A13, Def2 ;
::_thesis: verum
end;
supposethat A15: not x + z <=' y and
A16: ( not y <=' x & not y <=' z ) ; ::_thesis: (y -' z) - x = (y -' x) - z
A17: not z <=' y -' x by A1, A15, Lm8;
 ( not x <=' y -' z & x -' (y -' z) = z -' (y -' x) ) by A15, A16, Lm8, Lm13;
hence (y -' z) - x = [{},(z -' (y -' x))] by Def2
.= (y -' x) - z by A17, Def2 ;
::_thesis: verum
end;
end;
end;

theorem :: ARYTM_1:26
for z, y, x being Element of REAL+ st z <=' y holds
x *' (y -' z) = (x *' y) - (x *' z)
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( z <=' y implies x *' (y -' z) = (x *' y) - (x *' z) )
assume  z <=' y ; ::_thesis: x *' (y -' z) = (x *' y) - (x *' z)
then  x *' z <=' x *' y by Th8;
then  (x *' y) - (x *' z) = (x *' y) -' (x *' z) by Def2;
hence  x *' (y -' z) = (x *' y) - (x *' z) by Lm14; ::_thesis: verum
end;

theorem Th27: :: ARYTM_1:27
for z, y, x being Element of REAL+ st not z <=' y & x <> {} holds
[{},(x *' (z -' y))] = (x *' y) - (x *' z)
proof
let z, y, x be Element of REAL+ ; ::_thesis: ( not z <=' y & x <> {} implies [{},(x *' (z -' y))] = (x *' y) - (x *' z) )
assume  ( not z <=' y & x <> {} ) ; ::_thesis: [{},(x *' (z -' y))] = (x *' y) - (x *' z)
then A1: not x *' z <=' x *' y by Lm2;
thus [{},(x *' (z -' y))] = [{},((x *' z) -' (x *' y))] by Lm14
.= (x *' y) - (x *' z) by A1, Def2 ; ::_thesis: verum
end;

theorem :: ARYTM_1:28
for y, z, x being Element of REAL+ st y -' z <> {} & z <=' y & x <> {} holds
(x *' z) - (x *' y) = [{},(x *' (y -' z))]
proof
let y, z, x be Element of REAL+ ; ::_thesis: ( y -' z <> {} & z <=' y & x <> {} implies (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
assume  y -' z <> {} ; ::_thesis: ( not z <=' y or not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
then A1: y <> z by Lm3;
assume  z <=' y ; ::_thesis: ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
then  not y <=' z by A1, Th4;
hence  ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) by Th27; ::_thesis: verum
end;