:: ARYTM_1 semantic presentation

theorem E1: :: 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;

E2: for b1, b2, b3 being Element of REAL+ holds
( ( b1 *' b2 = b1 *' b3 ) implies ( not b1 <> {} or 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 :: 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 E3: :: 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 E4: :: 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 E1;
then c4 = {} by ARYTM_2:6;
hence c2 = c3 by E5, ARYTM_2:def 8;
end;

theorem E5: :: 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 E6: :: 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 E7: :: 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 E8: :: 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;

E9: for b1, b2, b3 being Element of REAL+ holds
( ( b1 *' b2 <=' b1 *' b3 ) implies ( not b1 <> {} or 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, E2;
hence c3 <=' c4 by ARYTM_2:20;
end;

definition
let c2, c3 be Element of REAL+ ;
func c1 -' c2 -> Element of REAL+ means :E10: :: 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 ) ) & ( ( b1 = {} & b2 = {} ) implies ( c3 <=' c2 or b1 = b2 ) ) );
by ARYTM_2:12;
end;

:: deftheorem E10 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 = {} ) ) );

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

theorem E12: :: 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 E10;
assume c2 -' c3 = {} ;
then c2 = c3 by E14, ARYTM_2:def 8;
hence not verum by E13;
end;

theorem :: 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 E12;
hence c2 = c3 by E13, E4;
end;

theorem E13: :: 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 E10;
hence c2 -' c3 <=' c2 by ARYTM_2:20;
end;
suppose not c3 <=' c2 ;
then c2 -' c3 = {} by E10;
hence c2 -' c3 <=' c2 by E6;
end;
end;
end;

E14: 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 E6;
thus c3 -' c2 = (c3 -' c2) + c2 by E15, ARYTM_2:def 8
.= c3 by E16, E10 ;
end;

E15: 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 E10;
end;

E16: 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 E13;
then (c3 -' (c3 -' c2)) + (c3 -' c2) = c3 by E10
.= (c3 -' c2) + c2 by E17, E10 ;
hence c3 -' (c3 -' c2) = c2 by ARYTM_2:12;
end;

E17: 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 E10;
hence ( c2 -' c3 <=' c4 iff c2 <=' c4 + c3 ) by E7;
end;
suppose E18: not c3 <=' c2 ;
then E19: c2 -' c3 = {} by E10;
c3 <=' c4 + c3 by ARYTM_2:20;
hence ( c2 -' c3 <=' c4 iff c2 <=' c4 + c3 ) by E18, E19, E3, E6;
end;
end;
end;

E18: 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 E10;
hence ( c4 + c2 <=' c3 iff c4 <=' c3 -' c2 ) by E7;
end;

E19: 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, E3;
then E22: c4 <=' c2 -' c3 by E20, E18;
((c2 -' c3) -' c4) + (c4 + c3) = (((c2 -' c3) -' c4) + c4) + c3 by ARYTM_2:7
.= (c2 -' c3) + c3 by E22, E10
.= c2 by E21, E10 ;
hence (c2 -' c3) -' c4 = c2 -' (c4 + c3) by E20, E10;
end;
suppose E20: c4 = {} ;
hence (c2 -' c3) -' c4 = c2 -' c3 by E14
.= 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, E10;
hence not verum by E21, E23, E5;
end;
c3 <=' c3 + c4 by ARYTM_2:20;
then E23: not c4 + c3 <=' c2 by E20, E3;
thus (c2 -' c3) -' c4 = {} by E22, E10
.= c2 -' (c4 + c3) by E23, E10 ;
end;
suppose that E20: not c4 + c3 <=' c2 and
E21: c3 <=' c2 ;
not c4 <=' c2 -' c3 by E20, E21, E18;
hence (c2 -' c3) -' c4 = {} by E10
.= c2 -' (c4 + c3) by E20, E10 ;

end;
end;
end;

E20: 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 E19
.= (c2 -' c4) -' c3 by E19 ;
end;

theorem :: 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, E10
.= ((c3 -' c2) + c2) + c4 by E21, E10
.= ((c3 -' c2) + c4) + c2 by ARYTM_2:7 ;
hence c3 + (c4 -' c2) = (c3 -' c2) + c4 by ARYTM_2:12;
end;

theorem E21: :: 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, E3;
(c4 + (c3 -' c2)) + c2 = c4 + ((c3 -' c2) + c2) by ARYTM_2:7
.= c4 + c3 by E22, E10
.= ((c4 + c3) -' c2) + c2 by E23, E10 ;
hence c4 + (c3 -' c2) = (c4 + c3) -' c2 by ARYTM_2:12;
end;

E22: 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 E17;
(c4 -' (c3 -' c2)) + (c3 -' c2) = c4 by E24, E10
.= (c4 + c3) -' c3 by E15
.= (c4 + (c2 + (c3 -' c2))) -' c3 by E23, E10
.= ((c4 + c2) + (c3 -' c2)) -' c3 by ARYTM_2:7
.= ((c4 + c2) -' c3) + (c3 -' c2) by E25, E21 ;
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 E17;
thus c4 -' (c3 -' c2) = {} by E24, E10
.= (c4 + c2) -' c3 by E25, E10 ;
end;
end;
end;

E23: 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, E22
.= (c3 -' c2) + c4 by E24, E21 ;
end;

E24: 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, E22
.= c4 -' (c3 -' c2) by E25, E22 ;
end;

theorem :: 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, E22
.= (c3 -' c2) + c4 by E25, E21 ;
end;

theorem :: 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, E10
.= ((c3 -' c2) + c2) + c4 by E25, E10
.= ((c3 -' c2) + c4) + c2 by ARYTM_2:7 ;
hence (c4 -' c2) + c3 = (c3 -' c2) + c4 by ARYTM_2:12;
end;

theorem :: 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, E3;
(c4 -' c3) + c2 <=' (c4 -' c3) + c3 by E25, E7;
then (c4 -' c3) + c2 <=' c4 by E26, E10;
then (c4 -' c3) + c2 <=' (c4 -' c2) + c2 by E27, E10;
hence c4 -' c3 <=' c4 -' c2 by E7;
end;
suppose not c3 <=' c4 ;
then c4 -' c3 = {} by E10;
hence c4 -' c3 <=' c4 -' c2 by E6;
end;
end;
end;

theorem :: 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, E3;
then ( (c2 -' c4) + c4 = c2 & (c3 -' c4) + c4 = c3 ) by E26, E10;
hence c2 -' c4 <=' c3 -' c4 by E25, E7;
end;
suppose not c4 <=' c2 ;
then c2 -' c4 = {} by E10;
hence c2 -' c4 <=' c3 -' c4 by E6;
end;
end;
end;

E25: 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 E8;
(c2 *' (c3 -' c4)) + (c2 *' c4) = c2 *' ((c3 -' c4) + c4) by ARYTM_2:14
.= c2 *' c3 by E26, E10
.= ((c2 *' c3) -' (c2 *' c4)) + (c2 *' c4) by E27, E10 ;
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, E14 ;

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

end;
end;
end;

definition
let c2, c3 be Element of REAL+ ;
func c1 - c2 -> set equals :E26: :: 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 E26 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 :: 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 E26;
hence c2 - c2 = {} by E11;
end;

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

end;

theorem :: 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, E3;
then (c4 + c3) - c2 = (c4 + c3) -' c2 by E26;
hence c4 + (c3 -' c2) = (c4 + c3) - c2 by E27, E21;
end;

theorem :: 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 E17;
then ( c4 - (c2 -' c3) = c4 -' (c2 -' c3) & (c4 + c3) - c2 = (c4 + c3) -' c2 ) by E28, E26;
hence c4 - (c2 -' c3) = (c4 + c3) - c2 by E27, E22;
end;
suppose E28: not c2 -' c3 <=' c4 ;
then E29: not c2 <=' c4 + c3 by E17;
(c2 -' c3) -' c4 = c2 -' (c4 + c3) by E19;
hence c4 - (c2 -' c3) = [{} ,(c2 -' (c4 + c3))] by E28, E26
.= (c4 + c3) - c2 by E29, E26 ;

end;
end;
end;

theorem :: ARYTM_1:22
for b1, b2, b3 being Element of REAL+ holds
( ( b1 <=' b2 ) implies ( b1 <=' b3 or 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 E13;
then c2 -' c4 <=' c3 by E27, E3;
then c3 - (c2 -' c4) = c3 -' (c2 -' c4) by E26;
hence c3 - (c2 -' c4) = (c3 -' c2) + c4 by E27, E28, E23;
end;

theorem :: ARYTM_1:23
for b1, b2, b3 being Element of REAL+ holds
( ( ) implies ( b1 <=' b2 or b1 <=' b3 or 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 E17;
then ( c3 - (c2 -' c4) = c3 -' (c2 -' c4) & c4 - (c2 -' c3) = c4 -' (c2 -' c3) ) by E26;
hence c3 - (c2 -' c4) = c4 - (c2 -' c3) by E27, E28, E24;
end;
suppose not c2 <=' c3 + c4 ;
then E29: ( not c2 -' c4 <=' c3 & not c2 -' c3 <=' c4 ) by E17;
(c2 -' c4) -' c3 = (c2 -' c3) -' c4 by E20;
hence c3 - (c2 -' c4) = [{} ,((c2 -' c3) -' c4)] by E29, E26
.= c4 - (c2 -' c3) by E29, E26 ;

end;
end;
end;

theorem :: 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, E18;
then ( c3 - (c2 + c4) = c3 -' (c2 + c4) & (c3 -' c2) - c4 = (c3 -' c2) -' c4 ) by E28, E26;
hence c3 - (c2 + c4) = (c3 -' c2) - c4 by E19;
end;
suppose that E28: not c2 + c4 <=' c3 and
E29: c3 <=' c2 ;
E30: not c4 <=' c3 -' c2 by E27, E28, E18;
E31: c3 = c2 by E27, E29, E4;
E32: c3 -' c3 = {} by E11;
(c3 + c4) -' c3 = c4 by E15
.= c4 -' (c3 -' c3) by E32, E14 ;
hence c3 - (c2 + c4) = [{} ,(c4 -' (c3 -' c2))] by E28, E31, E26
.= (c3 -' c2) - c4 by E30, E26 ;

end;
suppose that E28: not c2 + c4 <=' c3 and
E29: not c3 <=' c2 ;
E30: not c4 <=' c3 -' c2 by E27, E28, E18;
(c2 + c4) -' c3 = c4 -' (c3 -' c2) by E29, E22;
hence c3 - (c2 + c4) = [{} ,(c4 -' (c3 -' c2))] by E28, E26
.= (c3 -' c2) - c4 by E30, E26 ;

end;
end;
end;

theorem :: ARYTM_1:25
for b1, b2, b3 being Element of REAL+ holds
( ( b1 <=' b2 & b3 <=' b2 ) implies ( (b2 -' b3) - b1 = (b2 -' b1) - b3 ) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume that
E27: c2 <=' c3 and
E28: c4 <=' c3 ;
per cases not ( not c2 + c4 <=' c3 & not ( not c2 + c4 <=' c3 & c3 <=' c2 ) & not ( not c2 + c4 <=' c3 & c3 <=' c4 ) & not ( not c2 + c4 <=' c3 & not c3 <=' c2 & not c3 <=' c4 ) ) ;
suppose c2 + c4 <=' c3 ;
then ( c2 <=' c3 -' c4 & c4 <=' c3 -' c2 ) by E27, E28, E18;
then ( (c3 -' c4) -' c2 = (c3 -' c4) - c2 & (c3 -' c2) -' c4 = (c3 -' c2) - c4 ) by E26;
hence (c3 -' c4) - c2 = (c3 -' c2) - c4 by E20;
end;
suppose that E29: not c2 + c4 <=' c3 and
E30: c3 <=' c2 ;
E31: ( not c2 <=' c3 -' c4 & not c4 <=' c3 -' c2 ) by E27, E28, E29, E18;
E32: c2 -' c2 = {} by E11;
E33: c2 = c3 by E27, E30, E4;
then c2 -' (c2 -' c4) = c4 by E28, E16
.= c4 -' (c2 -' c2) by E32, E14 ;
hence (c3 -' c4) - c2 = [{} ,(c4 -' (c3 -' c2))] by E31, E33, E26
.= (c3 -' c2) - c4 by E31, E26 ;

end;
suppose that E29: not c2 + c4 <=' c3 and
E30: c3 <=' c4 ;
E31: ( not c2 <=' c3 -' c4 & not c4 <=' c3 -' c2 ) by E27, E28, E29, E18;
E32: c4 -' c4 = {} by E11;
E33: c4 = c3 by E28, E30, E4;
c2 -' (c4 -' c4) = c2 by E32, E14
.= c4 -' (c4 -' c2) by E27, E33, E16 ;
hence (c3 -' c4) - c2 = [{} ,(c4 -' (c3 -' c2))] by E31, E33, E26
.= (c3 -' c2) - c4 by E31, E26 ;

end;
suppose that E29: not c2 + c4 <=' c3 and
E30: ( not c3 <=' c2 & not c3 <=' c4 ) ;
E31: ( not c2 <=' c3 -' c4 & not c4 <=' c3 -' c2 ) by E27, E28, E29, E18;
c2 -' (c3 -' c4) = c4 -' (c3 -' c2) by E30, E24;
hence (c3 -' c4) - c2 = [{} ,(c4 -' (c3 -' c2))] by E31, E26
.= (c3 -' c2) - c4 by E31, E26 ;

end;
end;
end;

theorem :: ARYTM_1:26
for b1, b2, b3 being Element of REAL+ holds
( b1 <=' b2 implies b3 *' (b2 -' b1) = (b3 *' b2) - (b3 *' b1) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume c2 <=' c3 ;
then c4 *' c2 <=' c4 *' c3 by E8;
then (c4 *' c3) - (c4 *' c2) = (c4 *' c3) -' (c4 *' c2) by E26;
hence c4 *' (c3 -' c2) = (c4 *' c3) - (c4 *' c2) by E25;
end;

theorem E27: :: ARYTM_1:27
for b1, b2, b3 being Element of REAL+ holds
( ( ) implies ( b1 <=' b2 or not b3 <> {} or [{} ,(b3 *' (b1 -' b2))] = (b3 *' b2) - (b3 *' b1) ) )
proof
let c2, c3, c4 be Element of REAL+ ;
assume ( not c2 <=' c3 & c4 <> {} ) ;
then E28: not c4 *' c2 <=' c4 *' c3 by E9;
thus [{} ,(c4 *' (c2 -' c3))] = [{} ,((c4 *' c2) -' (c4 *' c3))] by E25
.= (c4 *' c3) - (c4 *' c2) by E28, E26 ;
end;

theorem :: ARYTM_1:28
for b1, b2, b3 being Element of REAL+ holds
( ( b2 <=' b1 ) implies ( not b1 -' b2 <> {} or not b3 <> {} or (b3 *' b2) - (b3 *' b1) = [{} ,(b3 *' (b1 -' b2))] ) )
proof
let c2, c3, c4 be Element of REAL+ ;