:: ARYTM_1 semantic presentation

theorem Th1: :: ARYTM_1:1
for b1, b2 being Element of REAL+ holds
( b1 + b2 = b2 implies b1 = {} )
proof
let c1, c2 be Element of REAL+ ;
reconsider c3 = {} as Element of REAL+ by ARYTM_2:21;
assume c1 + c2 = c2 ;
then c1 + c2 = c2 + c3 by ARYTM_2:def 8;
hence c1 = {} by ARYTM_2:12;
end;

reconsider c1 = one as Element of REAL+ by ARYTM_2:21;

Lemma2: for b1, b2, b3 being Element of REAL+ holds
( b1 *' b2 = b1 *' b3 & b1 <> {} implies b2 = b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E3: c2 *' c3 = c2 *' c4 ;
assume c2 <> {} ;
then consider c5 being Element of REAL+ such that
E4: c2 *' c5 = one by ARYTM_2:15;
thus c3 = (c2 *' c5) *' c3 by E4, ARYTM_2:16
.= c5 *' (c2 *' c4) by E3, ARYTM_2:13
.= (c2 *' c5) *' c4 by ARYTM_2:13
.= c4 by E4, ARYTM_2:16 ;
end;

theorem Th2: :: ARYTM_1:2
for b1, b2 being Element of REAL+ holds
not ( b1 *' b2 = {} & not b1 = {} & not b2 = {} )
proof
let c2, c3 be Element of REAL+ ;
assume E3: c2 *' c3 = {} ;
assume c2 <> {} ;
then consider c4 being Element of REAL+ such that
E4: c2 *' c4 = one by ARYTM_2:15;
thus c3 = (c2 *' c4) *' c3 by E4, ARYTM_2:16
.= (c2 *' c3) *' c4 by ARYTM_2:13
.= {} by E3, ARYTM_2:4 ;
end;

theorem Th3: :: ARYTM_1:3
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b2 <=' b3 implies b1 <=' b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume c2 <=' c3 ;
then consider c5 being Element of REAL+ such that
E4: c2 + c5 = c3 by ARYTM_2:10;
assume c3 <=' c4 ;
then consider c6 being Element of REAL+ such that
E5: c3 + c6 = c4 by ARYTM_2:10;
c4 = c2 + (c5 + c6) by E4, E5, ARYTM_2:7;
hence c2 <=' c4 by ARYTM_2:20;
end;

theorem Th4: :: ARYTM_1:4
for b1, b2 being Element of REAL+ holds
( b1 <=' b2 & b2 <=' b1 implies b1 = b2 )
proof
let c2, c3 be Element of REAL+ ;
assume c2 <=' c3 ;
then consider c4 being Element of REAL+ such that
E5: c2 + c4 = c3 by ARYTM_2:10;
assume c3 <=' c2 ;
then consider c5 being Element of REAL+ such that
E6: c3 + c5 = c2 by ARYTM_2:10;
c2 = c2 + (c4 + c5) by E5, E6, ARYTM_2:7;
then c4 + c5 = {} by Th1;
then c4 = {} by ARYTM_2:6;
hence c2 = c3 by E5, ARYTM_2:def 8;
end;

theorem Th5: :: ARYTM_1:5
for b1, b2 being Element of REAL+ holds
( b1 <=' b2 & b2 = {} implies b1 = {} )
proof
let c2, c3 be Element of REAL+ ;
assume c2 <=' c3 ;
then consider c4 being Element of REAL+ such that
E6: c2 + c4 = c3 by ARYTM_2:10;
thus not ( c3 = {} & not c2 = {} ) by E6, ARYTM_2:6;
end;

theorem Th6: :: ARYTM_1:6
for b1, b2 being Element of REAL+ holds
( b1 = {} implies b1 <=' b2 )
proof
let c2, c3 be Element of REAL+ ;
assume c2 = {} ;
then c2 + c3 = c3 by ARYTM_2:def 8;
hence c2 <=' c3 by ARYTM_2:20;
end;

theorem Th7: :: ARYTM_1:7
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 iff b1 + b3 <=' b2 + b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
thus ( c2 <=' c3 implies c2 + c4 <=' c3 + c4 )
proof
assume c2 <=' c3 ;
then consider c5 being Element of REAL+ such that
E8: c2 + c5 = c3 by ARYTM_2:10;
(c2 + c4) + c5 = c3 + c4 by E8, ARYTM_2:7;
hence c2 + c4 <=' c3 + c4 by ARYTM_2:20;
end;
assume c2 + c4 <=' c3 + c4 ;
then consider c5 being Element of REAL+ such that
E8: (c2 + c4) + c5 = c3 + c4 by ARYTM_2:10;
c3 + c4 = (c2 + c5) + c4 by E8, ARYTM_2:7;
then c3 = c2 + c5 by ARYTM_2:12;
hence c2 <=' c3 by ARYTM_2:20;
end;

theorem Th8: :: ARYTM_1:8
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b1 *' b3 <=' b2 *' b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume c2 <=' c3 ;
then consider c5 being Element of REAL+ such that
E9: c2 + c5 = c3 by ARYTM_2:10;
c3 *' c4 = (c2 *' c4) + (c5 *' c4) by E9, ARYTM_2:14;
hence c2 *' c4 <=' c3 *' c4 by ARYTM_2:20;
end;

Lemma9: for b1, b2, b3 being Element of REAL+ holds
( b1 *' b2 <=' b1 *' b3 & b1 <> {} implies b2 <=' b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume c2 *' c3 <=' c2 *' c4 ;
then consider c5 being Element of REAL+ such that
E10: (c2 *' c3) + c5 = c2 *' c4 by ARYTM_2:10;
assume E11: c2 <> {} ;
then consider c6 being Element of REAL+ such that
E12: c2 *' c6 = one by ARYTM_2:15;
c2 *' c4 = (c2 *' c3) + (c1 *' c5) by E10, ARYTM_2:16
.= (c2 *' c3) + (c2 *' (c6 *' c5)) by E12, ARYTM_2:13
.= c2 *' (c3 + (c6 *' c5)) by ARYTM_2:14 ;
then c4 = c3 + (c6 *' c5) by E11, Lemma2;
hence c3 <=' c4 by ARYTM_2:20;
end;

definition
let c2, c3 be Element of REAL+ ;
func c1 -' c2 -> Element of REAL+ means :Def1: :: ARYTM_1:def 1
a3 + a2 = a1 if a2 <=' a1
otherwise a3 = {} ;
existence
( not ( c3 <=' c2 & ( for b1 being Element of REAL+ holds
not b1 + c3 = c2 ) ) & not ( not c3 <=' c2 & ( for b1 being Element of REAL+ holds
not b1 = {} ) ) )
proof
hereby
assume c3 <=' c2 ;
then ex b1 being Element of REAL+ st c3 + b1 = c2 by ARYTM_2:10;
hence ex b1 being Element of REAL+ st b1 + c3 = c2 ;
end;
thus not ( not c3 <=' c2 & ( for b1 being Element of REAL+ holds
not b1 = {} ) ) by ARYTM_2:21;
end;
correctness
consistency
for b1 being Element of REAL+ holds
verum;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( c3 <=' c2 & b1 + c3 = c2 & b2 + c3 = c2 implies b1 = b2 ) & ( not c3 <=' c2 & b1 = {} & b2 = {} implies b1 = b2 ) );
by ARYTM_2:12;
end;

:: deftheorem Def1 defines -' ARYTM_1:def 1 :
for b1, b2, b3 being Element of REAL+ holds
( ( b2 <=' b1 implies ( b3 = b1 -' b2 iff b3 + b2 = b1 ) ) & ( not b2 <=' b1 implies ( b3 = b1 -' b2 iff b3 = {} ) ) );

Lemma11: for b1 being Element of REAL+ holds b1 -' b1 = {}
proof
let c2 be Element of REAL+ ;
c2 <=' c2 ;
then (c2 -' c2) + c2 = c2 by Def1;
hence c2 -' c2 = {} by Th1;
end;

theorem Th9: :: ARYTM_1:9
for b1, b2 being Element of REAL+ holds
not ( not b1 <=' b2 & not b1 -' b2 <> {} )
proof
let c2, c3 be Element of REAL+ ;
assume E13: not c2 <=' c3 ;
then E14: (c2 -' c3) + c3 = c2 by Def1;
assume c2 -' c3 = {} ;
then c2 = c3 by E14, ARYTM_2:def 8;
hence not verum by E13;
end;

theorem Th10: :: ARYTM_1:10
for b1, b2 being Element of REAL+ holds
( b1 <=' b2 & b2 -' b1 = {} implies b1 = b2 )
proof
let c2, c3 be Element of REAL+ ;
assume E13: c2 <=' c3 ;
assume c3 -' c2 = {} ;
then c3 <=' c2 by Th9;
hence c2 = c3 by E13, Th4;
end;

theorem Th11: :: ARYTM_1:11
for b1, b2 being Element of REAL+ holds b1 -' b2 <=' b1
proof
let c2, c3 be Element of REAL+ ;
per cases not ( not c3 <=' c2 & c3 <=' c2 ) ;
suppose c3 <=' c2 ;
then (c2 -' c3) + c3 = c2 by Def1;
hence c2 -' c3 <=' c2 by ARYTM_2:20;
end;
suppose not c3 <=' c2 ;
then c2 -' c3 = {} by Def1;
hence c2 -' c3 <=' c2 by Th6;
end;
end;
end;

Lemma14: for b1, b2 being Element of REAL+ holds
( b1 = {} implies b2 -' b1 = b2 )
proof
let c2, c3 be Element of REAL+ ;
assume E15: c2 = {} ;
then E16: c2 <=' c3 by Th6;
thus c3 -' c2 = (c3 -' c2) + c2 by E15, ARYTM_2:def 8
.= c3 by E16, Def1 ;
end;

Lemma15: for b1, b2 being Element of REAL+ holds (b1 + b2) -' b2 = b1
proof
let c2, c3 be Element of REAL+ ;
c3 <=' c2 + c3 by ARYTM_2:20;
hence (c2 + c3) -' c3 = c2 by Def1;
end;

Lemma16: for b1, b2 being Element of REAL+ holds
( b1 <=' b2 implies b2 -' (b2 -' b1) = b1 )
proof
let c2, c3 be Element of REAL+ ;
assume E17: c2 <=' c3 ;
c3 -' c2 <=' c3 by Th11;
then (c3 -' (c3 -' c2)) + (c3 -' c2) = c3 by Def1
.= (c3 -' c2) + c2 by E17, Def1 ;
hence c3 -' (c3 -' c2) = c2 by ARYTM_2:12;
end;

Lemma17: for b1, b2, b3 being Element of REAL+ holds
( b1 -' b2 <=' b3 iff b1 <=' b3 + b2 )
proof
let c2, c3, c4 be Element of REAL+ ;
per cases not ( not c3 <=' c2 & c3 <=' c2 ) ;
suppose c3 <=' c2 ;
then (c2 -' c3) + c3 = c2 by Def1;
hence ( c2 -' c3 <=' c4 iff c2 <=' c4 + c3 ) by Th7;
end;
suppose E18: not c3 <=' c2 ;
then E19: c2 -' c3 = {} by Def1;
c3 <=' c4 + c3 by ARYTM_2:20;
hence ( c2 -' c3 <=' c4 iff c2 <=' c4 + c3 ) by E18, E19, Th3, Th6;
end;
end;
end;

Lemma18: for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies ( b3 + b1 <=' b2 iff b3 <=' b2 -' b1 ) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume c2 <=' c3 ;
then (c3 -' c2) + c2 = c3 by Def1;
hence ( c4 + c2 <=' c3 iff c4 <=' c3 -' c2 ) by Th7;
end;

Lemma19: for b1, b2, b3 being Element of REAL+ holds (b1 -' b2) -' b3 = b1 -' (b3 + b2)
proof
let c2, c3, c4 be Element of REAL+ ;
per cases not ( not c4 + c3 <=' c2 & not c4 = {} & not ( not c3 <=' c2 & c4 <> {} ) & not ( not c4 + c3 <=' c2 & c3 <=' c2 ) ) ;
suppose E20: c4 + c3 <=' c2 ;
c3 <=' c4 + c3 by ARYTM_2:20;
then E21: c3 <=' c2 by E20, Th3;
then E22: c4 <=' c2 -' c3 by E20, Lemma18;
((c2 -' c3) -' c4) + (c4 + c3) = (((c2 -' c3) -' c4) + c4) + c3 by ARYTM_2:7
.= (c2 -' c3) + c3 by E22, Def1
.= c2 by E21, Def1 ;
hence (c2 -' c3) -' c4 = c2 -' (c4 + c3) by E20, Def1;
end;
suppose E20: c4 = {} ;
hence (c2 -' c3) -' c4 = c2 -' c3 by Lemma14
.= c2 -' (c4 + c3) by E20, ARYTM_2:def 8 ;

end;
suppose that E20: not c3 <=' c2 and
E21: c4 <> {} ;
E22: now
assume E23: c4 <=' c2 -' c3 ;
c2 -' c3 = {} by E20, Def1;
hence not verum by E21, E23, Th5;
end;
c3 <=' c3 + c4 by ARYTM_2:20;
then E23: not c4 + c3 <=' c2 by E20, Th3;
thus (c2 -' c3) -' c4 = {} by E22, Def1
.= c2 -' (c4 + c3) by E23, Def1 ;
end;
suppose that E20: not c4 + c3 <=' c2 and
E21: c3 <=' c2 ;
not c4 <=' c2 -' c3 by E20, E21, Lemma18;
hence (c2 -' c3) -' c4 = {} by Def1
.= c2 -' (c4 + c3) by E20, Def1 ;

end;
end;
end;

Lemma20: for b1, b2, b3 being Element of REAL+ holds (b1 -' b2) -' b3 = (b1 -' b3) -' b2
proof
let c2, c3, c4 be Element of REAL+ ;
thus (c2 -' c3) -' c4 = c2 -' (c4 + c3) by Lemma19
.= (c2 -' c4) -' c3 by Lemma19 ;
end;

theorem Th12: :: ARYTM_1:12
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b1 <=' b3 implies b2 + (b3 -' b1) = (b2 -' b1) + b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E21: c2 <=' c3 and
E22: c2 <=' c4 ;
(c3 + (c4 -' c2)) + c2 = c3 + ((c4 -' c2) + c2) by ARYTM_2:7
.= c3 + c4 by E22, Def1
.= ((c3 -' c2) + c2) + c4 by E21, Def1
.= ((c3 -' c2) + c4) + c2 by ARYTM_2:7 ;
hence c3 + (c4 -' c2) = (c3 -' c2) + c4 by ARYTM_2:12;
end;

theorem Th13: :: ARYTM_1:13
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b3 + (b2 -' b1) = (b3 + b2) -' b1 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E22: c2 <=' c3 ;
c3 <=' c4 + c3 by ARYTM_2:20;
then E23: c2 <=' c4 + c3 by E22, Th3;
(c4 + (c3 -' c2)) + c2 = c4 + ((c3 -' c2) + c2) by ARYTM_2:7
.= c4 + c3 by E22, Def1
.= ((c4 + c3) -' c2) + c2 by E23, Def1 ;
hence c4 + (c3 -' c2) = (c4 + c3) -' c2 by ARYTM_2:12;
end;

Lemma22: for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b3 -' (b2 -' b1) = (b3 + b1) -' b2 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E23: c2 <=' c3 ;
per cases not ( not c3 -' c2 <=' c4 & c3 -' c2 <=' c4 ) ;
suppose E24: c3 -' c2 <=' c4 ;
then E25: c3 <=' c4 + c2 by Lemma17;
(c4 -' (c3 -' c2)) + (c3 -' c2) = c4 by E24, Def1
.= (c4 + c3) -' c3 by Lemma15
.= (c4 + (c2 + (c3 -' c2))) -' c3 by E23, Def1
.= ((c4 + c2) + (c3 -' c2)) -' c3 by ARYTM_2:7
.= ((c4 + c2) -' c3) + (c3 -' c2) by E25, Th13 ;
hence c4 -' (c3 -' c2) = (c4 + c2) -' c3 by ARYTM_2:12;
end;
suppose E24: not c3 -' c2 <=' c4 ;
then E25: not c3 <=' c4 + c2 by Lemma17;
thus c4 -' (c3 -' c2) = {} by E24, Def1
.= (c4 + c2) -' c3 by E25, Def1 ;
end;
end;
end;

Lemma23: for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b3 <=' b1 implies b2 -' (b1 -' b3) = (b2 -' b1) + b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E24: c2 <=' c3 and
E25: c4 <=' c2 ;
thus c3 -' (c2 -' c4) = (c3 + c4) -' c2 by E25, Lemma22
.= (c3 -' c2) + c4 by E24, Th13 ;
end;

Lemma24: for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b3 <=' b2 implies b1 -' (b2 -' b3) = b3 -' (b2 -' b1) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E25: c2 <=' c3 and
E26: c4 <=' c3 ;
thus c2 -' (c3 -' c4) = (c2 + c4) -' c3 by E26, Lemma22
.= c4 -' (c3 -' c2) by E25, Lemma22 ;
end;

theorem Th14: :: ARYTM_1:14
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b3 <=' b1 implies (b2 -' b1) + b3 = b2 -' (b1 -' b3) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E25: c2 <=' c3 and
E26: c4 <=' c2 ;
thus c3 -' (c2 -' c4) = (c3 + c4) -' c2 by E26, Lemma22
.= (c3 -' c2) + c4 by E25, Th13 ;
end;

theorem Th15: :: ARYTM_1:15
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & b1 <=' b3 implies (b3 -' b1) + b2 = (b2 -' b1) + b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E25: c2 <=' c3 and
E26: c2 <=' c4 ;
((c4 -' c2) + c3) + c2 = ((c4 -' c2) + c2) + c3 by ARYTM_2:7
.= c4 + c3 by E26, Def1
.= ((c3 -' c2) + c2) + c4 by E25, Def1
.= ((c3 -' c2) + c4) + c2 by ARYTM_2:7 ;
hence (c4 -' c2) + c3 = (c3 -' c2) + c4 by ARYTM_2:12;
end;

theorem Th16: :: ARYTM_1:16
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b3 -' b2 <=' b3 -' b1 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E25: c2 <=' c3 ;
per cases not ( not c3 <=' c4 & c3 <=' c4 ) ;
suppose E26: c3 <=' c4 ;
then E27: c2 <=' c4 by E25, Th3;
(c4 -' c3) + c2 <=' (c4 -' c3) + c3 by E25, Th7;
then (c4 -' c3) + c2 <=' c4 by E26, Def1;
then (c4 -' c3) + c2 <=' (c4 -' c2) + c2 by E27, Def1;
hence c4 -' c3 <=' c4 -' c2 by Th7;
end;
suppose not c3 <=' c4 ;
then c4 -' c3 = {} by Def1;
hence c4 -' c3 <=' c4 -' c2 by Th6;
end;
end;
end;

theorem Th17: :: ARYTM_1:17
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b1 -' b3 <=' b2 -' b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E25: c2 <=' c3 ;
per cases not ( not c4 <=' c2 & c4 <=' c2 ) ;
suppose E26: c4 <=' c2 ;
then c4 <=' c3 by E25, Th3;
then ( (c2 -' c4) + c4 = c2 & (c3 -' c4) + c4 = c3 ) by E26, Def1;
hence c2 -' c4 <=' c3 -' c4 by E25, Th7;
end;
suppose not c4 <=' c2 ;
then c2 -' c4 = {} by Def1;
hence c2 -' c4 <=' c3 -' c4 by Th6;
end;
end;
end;

Lemma25: for b1, b2, b3 being Element of REAL+ holds b1 *' (b2 -' b3) = (b1 *' b2) -' (b1 *' b3)
proof
let c2, c3, c4 be Element of REAL+ ;
per cases not ( not c4 <=' c3 & not c2 = {} & not ( not c4 <=' c3 & c2 <> {} ) ) ;
suppose E26: c4 <=' c3 ;
then E27: c2 *' c4 <=' c2 *' c3 by Th8;
(c2 *' (c3 -' c4)) + (c2 *' c4) = c2 *' ((c3 -' c4) + c4) by ARYTM_2:14
.= c2 *' c3 by E26, Def1
.= ((c2 *' c3) -' (c2 *' c4)) + (c2 *' c4) by E27, Def1 ;
hence c2 *' (c3 -' c4) = (c2 *' c3) -' (c2 *' c4) by ARYTM_2:12;
end;
suppose E26: c2 = {} ;
then E27: ( c2 *' c3 = {} & c2 *' c4 = {} ) by ARYTM_2:4;
hence c2 *' (c3 -' c4) = c2 *' c3 by E26, ARYTM_2:4
.= (c2 *' c3) -' (c2 *' c4) by E27, Lemma14 ;

end;
suppose E26: ( not c4 <=' c3 & c2 <> {} ) ;
then E27: not c2 *' c4 <=' c2 *' c3 by Lemma9;
c3 -' c4 = {} by E26, Def1;
hence c2 *' (c3 -' c4) = {} by ARYTM_2:4
.= (c2 *' c3) -' (c2 *' c4) by E27, Def1 ;

end;
end;
end;

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

:: deftheorem Def2 defines - ARYTM_1:def 2 :
for b1, b2 being Element of REAL+ holds
( ( b2 <=' b1 implies b1 - b2 = b1 -' b2 ) & ( not b2 <=' b1 implies b1 - b2 = [{} ,(b2 -' b1)] ) );

theorem Th18: :: ARYTM_1:18
for b1 being Element of REAL+ holds b1 - b1 = {}
proof
let c2 be Element of REAL+ ;
c2 <=' c2 ;
then c2 - c2 = c2 -' c2 by Def2;
hence c2 - c2 = {} by Lemma11;
end;

theorem Th19: :: ARYTM_1:19
for b1, b2 being Element of REAL+ holds
( b1 = {} & b2 <> {} implies b1 - b2 = [{} ,b2] )
proof
let c2, c3 be Element of REAL+ ;
assume E27: ( c2 = {} & c3 <> {} ) ;
then c2 <=' c3 by Th6;
then not c3 <=' c2 by E27, Th4;
hence c2 - c3 = [{} ,(c3 -' c2)] by Def2
.= [{} ,c3] by E27, Lemma14 ;

end;

theorem Th20: :: ARYTM_1:20
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b3 + (b2 -' b1) = (b3 + b2) - b1 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E27: c2 <=' c3 ;
c3 <=' c4 + c3 by ARYTM_2:20;
then c2 <=' c4 + c3 by E27, Th3;
then (c4 + c3) - c2 = (c4 + c3) -' c2 by Def2;
hence c4 + (c3 -' c2) = (c4 + c3) - c2 by E27, Th13;
end;

theorem Th21: :: ARYTM_1:21
for b1, b2, b3 being Element of REAL+ holds
( not b1 <=' b2 implies b3 - (b1 -' b2) = (b3 + b2) - b1 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E27: not c2 <=' c3 ;
per cases not ( not c2 -' c3 <=' c4 & c2 -' c3 <=' c4 ) ;
suppose E28: c2 -' c3 <=' c4 ;
then c2 <=' c4 + c3 by Lemma17;
then ( c4 - (c2 -' c3) = c4 -' (c2 -' c3) & (c4 + c3) - c2 = (c4 + c3) -' c2 ) by E28, Def2;
hence c4 - (c2 -' c3) = (c4 + c3) - c2 by E27, Lemma22;
end;
suppose E28: not c2 -' c3 <=' c4 ;
then E29: not c2 <=' c4 + c3 by Lemma17;
(c2 -' c3) -' c4 = c2 -' (c4 + c3) by Lemma19;
hence c4 - (c2 -' c3) = [{} ,(c2 -' (c4 + c3))] by E28, Def2
.= (c4 + c3) - c2 by E29, Def2 ;

end;
end;
end;

theorem Th22: :: ARYTM_1:22
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 & not b1 <=' b3 implies b2 - (b1 -' b3) = (b2 -' b1) + b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E27: c2 <=' c3 and
E28: not c2 <=' c4 ;
c2 -' c4 <=' c2 by Th11;
then c2 -' c4 <=' c3 by E27, Th3;
then c3 - (c2 -' c4) = c3 -' (c2 -' c4) by Def2;
hence c3 - (c2 -' c4) = (c3 -' c2) + c4 by E27, E28, Lemma23;
end;

theorem Th23: :: ARYTM_1:23
for b1, b2, b3 being Element of REAL+ holds
( not b1 <=' b2 & not b1 <=' b3 implies b2 - (b1 -' b3) = b3 - (b1 -' b2) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E27: not c2 <=' c3 and
E28: not c2 <=' c4 ;
per cases not ( not c2 <=' c3 + c4 & c2 <=' c3 + c4 ) ;
suppose c2 <=' c3 + c4 ;
then ( c2 -' c4 <=' c3 & c2 -' c3 <=' c4 ) by Lemma17;
then ( c3 - (c2 -' c4) = c3 -' (c2 -' c4) & c4 - (c2 -' c3) = c4 -' (c2 -' c3) ) by Def2;
hence c3 - (c2 -' c4) = c4 - (c2 -' c3) by E27, E28, Lemma24;
end;
suppose not c2 <=' c3 + c4 ;
then E29: ( not c2 -' c4 <=' c3 & not c2 -' c3 <=' c4 ) by Lemma17;
(c2 -' c4) -' c3 = (c2 -' c3) -' c4 by Lemma20;
hence c3 - (c2 -' c4) = [{} ,((c2 -' c3) -' c4)] by E29, Def2
.= c4 - (c2 -' c3) by E29, Def2 ;

end;
end;
end;

theorem Th24: :: ARYTM_1:24
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b2 - (b1 + b3) = (b2 -' b1) - b3 )
proof
let c2, c3, c4 be Element of REAL+ ;
assume E27: c2 <=' c3 ;
per cases not ( not c2 + c4 <=' c3 & not ( not c2 + c4 <=' c3 & c3 <=' c2 ) & not ( not c2 + c4 <=' c3 & not c3 <=' c2 ) ) ;
suppose E28: c2 + c4 <=' c3 ;
then c4 <=' c3 -' c2 by E27, Lemma18;
then ( c3 - (c2 + c4) = c3 -' (c2 + c4) & (c3 -' c2) - c4 = (c3 -' c2) -' c4 ) by E28, Def2;
hence c3 - (c2 + c4) = (c3 -' c2) - c4 by Lemma19;
end;
suppose that E28: not c2 + c4 <=' c3 and
E29: c3 <=' c2 ;
E30: not c4 <=' c3 -' c2 by E27, E28, Lemma18;
E31: c3 = c2 by E27, E29, Th4;
E32: c3 -' c3 = {} by Lemma11;
(c3 + c4) -' c3 = c4 by Lemma15
.= c4 -' (c3 -' c3) by E32, Lemma14 ;
hence c3 - (c2 + c4) = [{} ,(c4 -' (c3 -' c2))]