:: XREAL_0 semantic presentation

begin

definition
let r be number ;
attrr is real  means :Def1: :: XREAL_0:def 1
r in REAL ;
end;

:: deftheorem Def1 defines real XREAL_0:def_1_:_
 for r being number holds
( r is real iff r in REAL );

registration
cluster  ->  real for Element of REAL ;
coherence
 for b1 being Element of REAL holds b1 is real
proof
let r be Element of REAL ; ::_thesis: r is real
thus  r in REAL ; :: according to XREAL_0:def_1 ::_thesis: verum
end;
end;

registration
cluster -infty  ->  non real ;
coherence
 not -infty is real
proof
A1: ( {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} ) by TARSKI:def_2;
assume  -infty in REAL ; :: according to XREAL_0:def_1 ::_thesis: contradiction
hence  contradiction by A1, XREGULAR:7; ::_thesis: verum
end;
cluster +infty  ->  non real ;
coherence
 not +infty is real
proof
thus  not +infty in REAL ; :: according to XREAL_0:def_1 ::_thesis: verum
end;
end;

registration
cluster natural  ->  real for set ;
coherence
 for b1 being number st b1 is natural holds
b1 is real
proof
let x be number ; ::_thesis: ( x is natural implies x is real )
assume  x is natural ; ::_thesis: x is real
then  x in NAT by ORDINAL1:def_12;
hence  x in REAL ; :: according to XREAL_0:def_1 ::_thesis: verum
end;
cluster real  ->  complex for set ;
coherence
 for b1 being number st b1 is real holds
b1 is complex
proof
let x be number ; ::_thesis: ( x is real implies x is complex )
assume  x is real ; ::_thesis: x is complex
then  x in REAL by Def1;
hence  x in COMPLEX by NUMBERS:def_2, XBOOLE_0:def_3; :: according to XCMPLX_0:def_2 ::_thesis: verum
end;
end;

registration
cluster real for set ;
existence
 ex b1 being number st b1 is real
proof
take  0 ; ::_thesis: 0 is real
thus  0 in REAL ; :: according to XREAL_0:def_1 ::_thesis: verum
end;
cluster real  ->  ext-real for set ;
coherence
 for b1 being number st b1 is real holds
b1 is ext-real
proof
let n be number ; ::_thesis: ( n is real implies n is ext-real )
assume  n in REAL ; :: according to XREAL_0:def_1 ::_thesis: n is ext-real
hence  n in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum
end;
end;

Lm1:  for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
proof
let x be real number ; ::_thesis: for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
let x1, x2 be Element of REAL ; ::_thesis: ( x = [*x1,x2*] implies ( x2 = 0 & x = x1 ) )
assume A1: x = [*x1,x2*] ; ::_thesis: ( x2 = 0 & x = x1 )
A2: x in REAL by Def1;
hereby  ::_thesis: x = x1
assume  x2 <> 0 ; ::_thesis: contradiction
then  x = (0,1) --> (x1,x2) by A1, ARYTM_0:def_5;
hence  contradiction by A2, ARYTM_0:8; ::_thesis: verum
end;
hence  x = x1 by A1, ARYTM_0:def_5; ::_thesis: verum
end;

registration
let x be real number ;
cluster - x ->  real ;
coherence
 - x is real
proof
 x + (- x) = 0 ;
then consider x1, x2, y1, y2 being Element of REAL  such that
A1: x = [*x1,x2*] and
A2: - x = [*y1,y2*] and
A3: 0 = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
 ( + (x2,y2) = 0 & x2 = 0 ) by A1, A3, Lm1;
then  y2 = 0 by ARYTM_0:11;
hence  - x is real by A2, ARYTM_0:def_5; ::_thesis: verum
end;
clusterx "  ->  real ;
coherence
 x " is real
proof
percases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; ::_thesis: x " is real
hence  x " is real by XCMPLX_0:def_7; ::_thesis: verum
end;
supposeA4: x <> 0 ; ::_thesis: x " is real
then  x * (x ") = 1 by XCMPLX_0:def_7;
then consider x1, x2, y1, y2 being Element of REAL  such that
A5: x = [*x1,x2*] and
A6: x " = [*y1,y2*] and
A7: 1 = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
 ( + ((* (x1,y2)),(* (x2,y1))) = 0 & x2 = 0 ) by A5, A7, Lm1;
then  0 = * (x1,y2) by ARYTM_0:11, ARYTM_0:12;
then  ( x1 = 0 or y2 = 0 ) by ARYTM_0:21;
hence  x " is real by A4, A5, A6, Lm1, ARYTM_0:def_5; ::_thesis: verum
end;
end;
end;
let y be real number ;
clusterx + y ->  real ;
coherence
 x + y is real
proof
consider x1, x2, y1, y2 being Element of REAL  such that
A8: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A9: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
 ( x2 = 0 & y2 = 0 ) by A8, Lm1;
then  + (x2,y2) = 0 by ARYTM_0:11;
hence  x + y is real by A9, ARYTM_0:def_5; ::_thesis: verum
end;
clusterx * y ->  real ;
coherence
 x * y is real
proof
consider x1, x2, y1, y2 being Element of REAL  such that
A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
 x2 = 0 by A10, Lm1;
then A13: * (x2,y1) = 0 by ARYTM_0:12;
A14: y2 = 0 by A11, Lm1;
then  * ((opp x2),y2) = 0 by ARYTM_0:12;
then A15: opp (* (x2,y2)) = 0 by ARYTM_0:15;
 * (x1,y2) = 0 by A14, ARYTM_0:12;
then  + ((* (x1,y2)),(* (x2,y1))) = 0 by A13, ARYTM_0:11;
then x * y = + ((* (x1,y1)),0) by A12, A15, ARYTM_0:def_5
.= * (x1,y1) by ARYTM_0:11 ;
hence  x * y is real ; ::_thesis: verum
end;
end;

registration
let x, y be real number ;
clusterx - y ->  real ;
coherence
 x - y is real ;
clusterx / y ->  real ;
coherence
 x / y is real ;
end;

begin

   Lm2:  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
proof
let r, s be real number ; ::_thesis: ( ( ( 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+:] ) ) implies r <= s )
assume A1: ( ( 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+:] ) ) ; ::_thesis: r <= s
percases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) or ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ) ;
:: according to XXREAL_0:def_5
case ( r in REAL+ & s in REAL+ ) ; ::_thesis: ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 )
hence  ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
case ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ; ::_thesis: ex b1, b2 being Element of REAL+ st
( r = [0,b1] & s = [0,b2] & b2 <=' b1 )
hence  ex b1, b2 being Element of REAL+ st
( r = [0,b1] & s = [0,b2] & b2 <=' b1 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
case ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ; ::_thesis: ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty )
hence  ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty ) by A1; ::_thesis: verum
end;
end;
end;

Lm3:  {} in {{}}
by TARSKI:def_1;

Lm4:  for r, s being real number st r <= s & s <= r holds
r = s
proof
let r, s be real number ; ::_thesis: ( r <= s & s <= r implies r = s )
assume that
A1: r <= s and
A2: s <= r ; ::_thesis: r = s
A3: ( r in REAL & s in REAL ) by Def1;
percases ( ( r in REAL+ & s in REAL+ ) or ( r in REAL+ & s in [:{0},REAL+:] ) or ( s in REAL+ & r in [:{0},REAL+:] ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ) by A3, NUMBERS:def_1, XBOOLE_0:def_3;
suppose ( r in REAL+ & s in REAL+ ) ; ::_thesis: r = s
then  ( ex r9, s9 being Element of REAL+ st
( r = r9 & s = s9 & r9 <=' s9 ) & ex s99, r99 being Element of REAL+ st
( s = s99 & r = r99 & s99 <=' r99 ) ) by A1, A2, XXREAL_0:def_5;
hence  r = s by ARYTM_1:4; ::_thesis: verum
end;
supposeA4: ( r in REAL+ & s in [:{0},REAL+:] ) ; ::_thesis: r = s
then  ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  r = s by A1, A4, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA5: ( s in REAL+ & r in [:{0},REAL+:] ) ; ::_thesis: r = s
then  ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  r = s by A2, A5, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA6: ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ; ::_thesis: r = s
consider r9, s9 being Element of REAL+  such that
A7: ( r = [0,r9] & s = [0,s9] ) and
A8: s9 <=' r9 by A1, A6, XXREAL_0:def_5;
consider s99, r99 being Element of REAL+  such that
A9: ( s = [0,s99] & r = [0,r99] ) and
A10: r99 <=' s99 by A2, A6, XXREAL_0:def_5;
 ( r9 = r99 & s9 = s99 ) by A7, A9, XTUPLE_0:1;
hence  r = s by A8, A9, A10, ARYTM_1:4; ::_thesis: verum
end;
end;
end;

Lm5:  for r, s, t being real number st r <= s holds
r + t <= s + t
proof
let r, s, t be real number ; ::_thesis: ( r <= s implies r + t <= s + t )
reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;
A1: for x9 being Element of REAL
for r being real number st x9 = r holds
+ (x9,z1) = r + t
proof
let x9 be Element of REAL ; ::_thesis: for r being real number st x9 = r holds
+ (x9,z1) = r + t
let r be real number ; ::_thesis: ( x9 = r implies + (x9,z1) = r + t )
assume A2: x9 = r ; ::_thesis: + (x9,z1) = r + t
consider x1, x2, y1, y2 being Element of REAL  such that
A3: ( r = [*x1,x2*] & t = [*y1,y2*] ) and
A4: r + t = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
 ( x2 = 0 & y2 = 0 ) by A3, Lm1;
then A5: + (x2,y2) = 0 by ARYTM_0:11;
 ( r = x1 & t = y1 ) by A3, Lm1;
hence  + (x9,z1) = r + t by A2, A4, A5, ARYTM_0:def_5; ::_thesis: verum
end;
then A6: + (y1,z1) = s + t ;
A7: + (x1,z1) = r + t by A1;
assume A8: r <= s ; ::_thesis: r + t <= s + t
percases ( ( r in REAL+ & s in REAL+ & t in REAL+ ) or ( r in [:{0},REAL+:] & s in REAL+ & t in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & t in REAL+ ) or ( r in REAL+ & s in REAL+ & t in [:{0},REAL+:] ) or ( r in [:{0},REAL+:] & s in REAL+ & t in [:{0},REAL+:] ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & t in [:{0},REAL+:] ) ) by A8, XXREAL_0:def_5;
supposethat A9: r in REAL+ and
A10: s in REAL+ and
A11: t in REAL+ ; ::_thesis: r + t <= s + t
consider s9, t99 being Element of REAL+  such that
A12: ( s = s9 & t = t99 ) and
A13: + (y1,z1) = s9 + t99 by A10, A11, ARYTM_0:def_1;
consider x9, t9 being Element of REAL+  such that
A14: ( r = x9 & t = t9 ) and
A15: + (x1,z1) = x9 + t9 by A9, A11, ARYTM_0:def_1;
 ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by A8, A9, A10, XXREAL_0:def_5;
then  x9 + t9 <=' s9 + t99 by A14, A12, ARYTM_1:7;
hence  r + t <= s + t by A6, A7, A15, A13, Lm2; ::_thesis: verum
end;
supposethat A16: r in [:{0},REAL+:] and
A17: s in REAL+ and
A18: t in REAL+ ; ::_thesis: r + t <= s + t
consider s9, t99 being Element of REAL+  such that
 s = s9 and
A19: t = t99 and
A20: + (y1,z1) = s9 + t99 by A17, A18, ARYTM_0:def_1;
consider x9, t9 being Element of REAL+  such that
 r = [0,x9] and
A21: t = t9 and
A22: + (x1,z1) = t9 - x9 by A16, A18, ARYTM_0:def_1;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( x9 <=' t9 or not x9 <=' t9 ) ;
supposeA23: x9 <=' t9 ; ::_thesis: r + t <= s + t
 ( t9 -' x9 <=' t9 & t9 <=' s9 + t99 ) by A21, A19, ARYTM_1:11, ARYTM_2:19;
then A24: t9 -' x9 <=' s9 + t99 by ARYTM_1:3;
 t9 - x9 = t9 -' x9 by A23, ARYTM_1:def_2;
hence  r + t <= s + t by A6, A7, A22, A20, A24, Lm2; ::_thesis: verum
end;
suppose not x9 <=' t9 ; ::_thesis: r + t <= s + t
then  t9 - x9 = [0,(x9 -' t9)] by ARYTM_1:def_2;
then  t9 - x9 in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
then A25: not r + t in REAL+ by A7, A22, ARYTM_0:5, XBOOLE_0:3;
 not s + t in [:{0},REAL+:] by A6, A20, ARYTM_0:5, XBOOLE_0:3;
hence  r + t <= s + t by A25, XXREAL_0:def_5; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
supposethat A26: r in [:{0},REAL+:] and
A27: s in [:{0},REAL+:] and
A28: t in REAL+ ; ::_thesis: r + t <= s + t
consider s9, t99 being Element of REAL+  such that
A29: s = [0,s9] and
A30: t = t99 and
A31: + (y1,z1) = t99 - s9 by A27, A28, ARYTM_0:def_1;
consider x99, s99 being Element of REAL+  such that
A32: r = [0,x99] and
A33: s = [0,s99] and
A34: s99 <=' x99 by A8, A26, A27, XXREAL_0:def_5;
consider x9, t9 being Element of REAL+  such that
A35: r = [0,x9] and
A36: t = t9 and
A37: + (x1,z1) = t9 - x9 by A26, A28, ARYTM_0:def_1;
A38: x9 = x99 by A32, A35, XTUPLE_0:1;
A39: s9 = s99 by A33, A29, XTUPLE_0:1;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( x9 <=' t9 or not x9 <=' t9 ) ;
supposeA40: x9 <=' t9 ; ::_thesis: r + t <= s + t
then  s9 <=' t9 by A34, A38, A39, ARYTM_1:3;
then A41: t9 - s9 = t9 -' s9 by ARYTM_1:def_2;
A42: t9 - x9 = t9 -' x9 by A40, ARYTM_1:def_2;
 t9 -' x9 <=' t99 -' s9 by A34, A36, A30, A38, A39, ARYTM_1:16;
hence  r + t <= s + t by A6, A7, A36, A37, A30, A31, A42, A41, Lm2; ::_thesis: verum
end;
suppose not x9 <=' t9 ; ::_thesis: r + t <= s + t
then A43: + (x1,z1) = [0,(x9 -' t9)] by A37, ARYTM_1:def_2;
then A44: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( s9 <=' t9 or not s9 <=' t9 ) ;
suppose s9 <=' t9 ; ::_thesis: r + t <= s + t
then  t9 - s9 = t9 -' s9 by ARYTM_1:def_2;
then A45: not + (y1,z1) in [:{0},REAL+:] by A36, A30, A31, ARYTM_0:5, XBOOLE_0:3;
 not + (x1,z1) in REAL+ by A44, ARYTM_0:5, XBOOLE_0:3;
hence  r + t <= s + t by A6, A7, A45, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA46: not s9 <=' t9 ; ::_thesis: r + t <= s + t
A47: s9 -' t9 <=' x9 -' t9 by A34, A38, A39, ARYTM_1:17;
A48: + (y1,z1) = [0,(s9 -' t9)] by A36, A30, A31, A46, ARYTM_1:def_2;
then  + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
hence  r + t <= s + t by A6, A7, A43, A44, A48, A47, Lm2; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
supposethat A49: r in REAL+ and
A50: s in REAL+ and
A51: t in [:{0},REAL+:] ; ::_thesis: r + t <= s + t
consider s9, t99 being Element of REAL+  such that
A52: s = s9 and
A53: t = [0,t99] and
A54: + (y1,z1) = s9 - t99 by A50, A51, ARYTM_0:def_1;
consider x9, t9 being Element of REAL+  such that
A55: r = x9 and
A56: t = [0,t9] and
A57: + (x1,z1) = x9 - t9 by A49, A51, ARYTM_0:def_1;
A58: t9 = t99 by A56, A53, XTUPLE_0:1;
A59: ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by A8, A49, A50, XXREAL_0:def_5;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( t9 <=' x9 or not t9 <=' x9 ) ;
supposeA60: t9 <=' x9 ; ::_thesis: r + t <= s + t
then  t9 <=' s9 by A59, A55, A52, ARYTM_1:3;
then A61: s9 - t9 = s9 -' t9 by ARYTM_1:def_2;
A62: x9 - t9 = x9 -' t9 by A60, ARYTM_1:def_2;
 x9 -' t9 <=' s9 -' t99 by A59, A55, A52, A58, ARYTM_1:17;
hence  r + t <= s + t by A6, A7, A57, A54, A58, A62, A61, Lm2; ::_thesis: verum
end;
suppose not t9 <=' x9 ; ::_thesis: r + t <= s + t
then A63: + (x1,z1) = [0,(t9 -' x9)] by A57, ARYTM_1:def_2;
then A64: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( t9 <=' s9 or not t9 <=' s9 ) ;
suppose t9 <=' s9 ; ::_thesis: r + t <= s + t
then  s9 - t9 = s9 -' t9 by ARYTM_1:def_2;
then A65: not + (y1,z1) in [:{0},REAL+:] by A54, A58, ARYTM_0:5, XBOOLE_0:3;
 not + (x1,z1) in REAL+ by A64, ARYTM_0:5, XBOOLE_0:3;
hence  r + t <= s + t by A6, A7, A65, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA66: not t9 <=' s9 ; ::_thesis: r + t <= s + t
A67: t9 -' s9 <=' t9 -' x9 by A59, A55, A52, ARYTM_1:16;
A68: + (y1,z1) = [0,(t9 -' s9)] by A54, A58, A66, ARYTM_1:def_2;
then  + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
hence  r + t <= s + t by A6, A7, A63, A64, A68, A67, Lm2; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
supposethat A69: r in [:{0},REAL+:] and
A70: s in REAL+ and
A71: t in [:{0},REAL+:] ; ::_thesis: r + t <= s + t
 ( not r in REAL+ & not t in REAL+ ) by A69, A71, ARYTM_0:5, XBOOLE_0:3;
then consider x9, t9 being Element of REAL+  such that
 r = [0,x9] and
A72: t = [0,t9] and
A73: + (x1,z1) = [0,(x9 + t9)] by ARYTM_0:def_1;
A74: + (x1,z1) in [:{0},REAL+:] by A73, Lm3, ZFMISC_1:87;
consider s9, t99 being Element of REAL+  such that
 s = s9 and
A75: t = [0,t99] and
A76: + (y1,z1) = s9 - t99 by A70, A71, ARYTM_0:def_1;
A77: t9 = t99 by A72, A75, XTUPLE_0:1;
now__::_thesis:_r_+_t_<=_s_+_t
percases ( t9 <=' s9 or not t9 <=' s9 ) ;
suppose t9 <=' s9 ; ::_thesis: r + t <= s + t
then  s9 - t99 = s9 -' t99 by A77, ARYTM_1:def_2;
then A78: not + (y1,z1) in [:{0},REAL+:] by A76, ARYTM_0:5, XBOOLE_0:3;
 not + (x1,z1) in REAL+ by A74, ARYTM_0:5, XBOOLE_0:3;
hence  r + t <= s + t by A6, A7, A78, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA79: not t9 <=' s9 ; ::_thesis: r + t <= s + t
 ( t9 -' s9 <=' t9 & t9 <=' t9 + x9 ) by ARYTM_1:11, ARYTM_2:19;
then A80: t9 -' s9 <=' t9 + x9 by ARYTM_1:3;
A81: + (y1,z1) = [0,(t9 -' s9)] by A76, A77, A79, ARYTM_1:def_2;
then  + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
hence  r + t <= s + t by A6, A7, A73, A74, A81, A80, Lm2; ::_thesis: verum
end;
end;
end;
hence  r + t <= s + t ; ::_thesis: verum
end;
supposethat A82: r in [:{0},REAL+:] and
A83: s in [:{0},REAL+:] and
A84: t in [:{0},REAL+:] ; ::_thesis: r + t <= s + t
 ( not s in REAL+ & not t in REAL+ ) by A83, A84, ARYTM_0:5, XBOOLE_0:3;
then consider s9, t99 being Element of REAL+  such that
A85: s = [0,s9] and
A86: t = [0,t99] and
A87: + (y1,z1) = [0,(s9 + t99)] by ARYTM_0:def_1;
A88: + (y1,z1) in [:{0},REAL+:] by A87, Lm3, ZFMISC_1:87;
 ( not r in REAL+ & not t in REAL+ ) by A82, A84, ARYTM_0:5, XBOOLE_0:3;
then consider x9, t9 being Element of REAL+  such that
A89: r = [0,x9] and
A90: t = [0,t9] and
A91: + (x1,z1) = [0,(x9 + t9)] by ARYTM_0:def_1;
A92: + (x1,z1) in [:{0},REAL+:] by A91, Lm3, ZFMISC_1:87;
A93: t9 = t99 by A90, A86, XTUPLE_0:1;
consider x99, s99 being Element of REAL+  such that
A94: r = [0,x99] and
A95: s = [0,s99] and
A96: s99 <=' x99 by A8, A82, A83, XXREAL_0:def_5;
A97: s9 = s99 by A95, A85, XTUPLE_0:1;
 x9 = x99 by A94, A89, XTUPLE_0:1;
then  s9 + t9 <=' x9 + t99 by A96, A97, A93, ARYTM_1:7;
hence  r + t <= s + t by A6, A7, A91, A87, A93, A92, A88, Lm2; ::_thesis: verum
end;
end;
end;

Lm6:  for r, s, t being real number st r <= s & s <= t holds
r <= t
proof
let r, s, t be real number ; ::_thesis: ( r <= s & s <= t implies r <= t )
assume that
A1: r <= s and
A2: s <= t ; ::_thesis: r <= t
A3: ( r in REAL & s in REAL ) by Def1;
A4: t in REAL by Def1;
percases ( ( r in REAL+ & s in REAL+ & t in REAL+ ) or ( r in REAL+ & s in [:{0},REAL+:] ) or ( s in REAL+ & t in [:{0},REAL+:] ) or ( r in [:{0},REAL+:] & t in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] & t in [:{0},REAL+:] ) ) by A3, A4, NUMBERS:def_1, XBOOLE_0:def_3;
supposethat A5: r in REAL+ and
A6: s in REAL+ and
A7: t in REAL+ ; ::_thesis: r <= t
consider s99, t9 being Element of REAL+  such that
A8: s = s99 and
A9: t = t9 and
A10: s99 <=' t9 by A2, A6, A7, XXREAL_0:def_5;
consider x9, s9 being Element of REAL+  such that
A11: r = x9 and
A12: ( s = s9 & x9 <=' s9 ) by A1, A5, A6, XXREAL_0:def_5;
 x9 <=' t9 by A12, A8, A10, ARYTM_1:3;
hence  r <= t by A11, A9, Lm2; ::_thesis: verum
end;
supposeA13: ( r in REAL+ & s in [:{0},REAL+:] ) ; ::_thesis: r <= t
then  ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  r <= t by A1, A13, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA14: ( s in REAL+ & t in [:{0},REAL+:] ) ; ::_thesis: r <= t
then  ( ( not t in REAL+ or not s in REAL+ ) & ( not t in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  r <= t by A2, A14, XXREAL_0:def_5; ::_thesis: verum
end;
supposethat A15: r in [:{0},REAL+:] and
A16: t in REAL+ ; ::_thesis: r <= t
 ( ( not r in REAL+ or not t in REAL+ ) & ( not r in [:{0},REAL+:] or not t in [:{0},REAL+:] ) ) by A15, A16, ARYTM_0:5, XBOOLE_0:3;
hence  r <= t by A16, XXREAL_0:def_5; ::_thesis: verum
end;
supposethat A17: r in [:{0},REAL+:] and
A18: s in [:{0},REAL+:] and
A19: t in [:{0},REAL+:] ; ::_thesis: r <= t
consider s99, t9 being Element of REAL+  such that
A20: s = [0,s99] and
A21: t = [0,t9] and
A22: t9 <=' s99 by A2, A18, A19, XXREAL_0:def_5;
consider x9, s9 being Element of REAL+  such that
A23: r = [0,x9] and
A24: s = [0,s9] and
A25: s9 <=' x9 by A1, A17, A18, XXREAL_0:def_5;
 s9 = s99 by A24, A20, XTUPLE_0:1;
then  t9 <=' x9 by A25, A22, ARYTM_1:3;
hence  r <= t by A17, A19, A23, A21, Lm2; ::_thesis: verum
end;
end;
end;

reconsider z = 0 as Element of REAL+ by ARYTM_2:20;

Lm7:  not 0 in [:{0},REAL+:]
by ARYTM_0:5, ARYTM_2:20, XBOOLE_0:3;

reconsider j = 1 as Element of REAL+ by ARYTM_2:20;

 z <=' j
by ARYTM_1:6;

then Lm8:  0 <= 1
by Lm2;

 1 + (- 1) = 0
;

then consider x1, x2, y1, y2 being Element of REAL  such that
Lm9:  1 = [*x1,x2*] and
Lm10:  ( - 1 = [*y1,y2*] & 0 = [*(+ (x1,y1)),(+ (x2,y2))*] ) by XCMPLX_0:def_4;

Lm11:  x1 = 1
by Lm1, Lm9;

Lm12:  ( y1 = - 1 & + (x1,y1) = 0 )
by Lm1, Lm10;

Lm13: now__::_thesis:_not_-_1_in_REAL+
assume  - 1 in REAL+ ; ::_thesis: contradiction
then  ex x9, y9 being Element of REAL+ st
( x1 = x9 & y1 = y9 & z = x9 + y9 ) by Lm11, Lm12, ARYTM_0:def_1, ARYTM_2:20;
hence  contradiction by Lm11, ARYTM_2:5; ::_thesis: verum
end;

Lm14:  for r, s being real number st r >= 0 & s > 0 holds
r + s > 0
proof
let r, s be real number ; ::_thesis: ( r >= 0 & s > 0 implies r + s > 0 )
assume  r >= 0 ; ::_thesis: ( not s > 0 or r + s > 0 )
then  r + s >= 0 + s by Lm5;
hence  ( not s > 0 or r + s > 0 ) by Lm6; ::_thesis: verum
end;

Lm15:  for r, s being real number st r <= 0 & s < 0 holds
r + s < 0
proof
let r, s be real number ; ::_thesis: ( r <= 0 & s < 0 implies r + s < 0 )
assume  r <= 0 ; ::_thesis: ( not s < 0 or r + s < 0 )
then  r + s <= 0 + s by Lm5;
hence  ( not s < 0 or r + s < 0 ) by Lm6; ::_thesis: verum
end;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

Lm16:  for r, s, t being real number st r <= s & 0 <= t holds
r * t <= s * t
proof
let r, s, t be real number ; ::_thesis: ( r <= s & 0 <= t implies r * t <= s * t )
reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;
assume that
A1: r <= s and
A2: 0 <= t ; ::_thesis: r * t <= s * t
 not o in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
then A3: t in REAL+ by A2, XXREAL_0:def_5;
 for x9 being Element of REAL
for r being real number st x9 = r holds
* (x9,z1) = r * t
proof
let x9 be Element of REAL ; ::_thesis: for r being real number st x9 = r holds
* (x9,z1) = r * t
let r be real number ; ::_thesis: ( x9 = r implies * (x9,z1) = r * t )
assume A4: x9 = r ; ::_thesis: * (x9,z1) = r * t
consider x1, x2, y1, y2 being Element of REAL  such that
A5: r = [*x1,x2*] and
A6: t = [*y1,y2*] and
A7: r * t = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
 x2 = 0 by A5, Lm1;
then A8: * (x2,y1) = 0 by ARYTM_0:12;
A9: y2 = 0 by A6, Lm1;
then  * (x1,y2) = 0 by ARYTM_0:12;
then A10: + ((* (x1,y2)),(* (x2,y1))) = 0 by A8, ARYTM_0:11;
 ( r = x1 & t = y1 ) by A5, A6, Lm1;
hence  * (x9,z1) = + ((* (x1,y1)),(* ((opp x2),y2))) by A4, A9, ARYTM_0:11, ARYTM_0:12
.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15
.= r * t by A7, A10, ARYTM_0:def_5 ;
::_thesis: verum
end;
then A11: ( * (y1,z1) = s * t & * (x1,z1) = r * t ) ;
assume A12: not r * t <= s * t ; ::_thesis: contradiction
then A13: t <> 0 ;
percases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0},REAL+:] & s in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ) by A1, XXREAL_0:def_5;
supposethat A14: r in REAL+ and
A15: s in REAL+ ; ::_thesis: contradiction
consider s9, t99 being Element of REAL+  such that
A16: s = s9 and
A17: ( t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A15, ARYTM_0:def_2;
consider x9, t9 being Element of REAL+  such that
A18: r = x9 and
A19: ( t = t9 & * (x1,z1) = x9 *' t9 ) by A3, A14, ARYTM_0:def_2;
 ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by A1, A14, A15, XXREAL_0:def_5;
then  x9 *' t9 <=' s9 *' t9 by A18, A16, ARYTM_1:8;
hence  contradiction by A11, A12, A19, A17, Lm2; ::_thesis: verum
end;
supposethat A20: r in [:{0},REAL+:] and
A21: s in REAL+ ; ::_thesis: contradiction
 ex x9, t9 being Element of REAL+ st
( r = [0,x9] & t = t9 & * (x1,z1) = [0,(t9 *' x9)] ) by A3, A13, A20, ARYTM_0:def_2;
then  * (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;
then A22: not * (x1,z1) in REAL+ by ARYTM_0:5, XBOOLE_0:3;
 ex s9, t99 being Element of REAL+ st
( s = s9 & t = t99 & * (y1,z1) = s9 *' t99 ) by A3, A21, ARYTM_0:def_2;
then  not * (y1,z1) in [:{0},REAL+:] by ARYTM_0:5, XBOOLE_0:3;
hence  contradiction by A11, A12, A22, XXREAL_0:def_5; ::_thesis: verum
end;
supposethat A23: r in [:{0},REAL+:] and
A24: s in [:{0},REAL+:] ; ::_thesis: contradiction
consider s9, t99 being Element of REAL+  such that
A25: s = [0,s9] and
A26: t = t99 and
A27: * (y1,z1) = [0,(t99 *' s9)] by A3, A13, A24, ARYTM_0:def_2;
A28: * (y1,z1) in [:{0},REAL+:] by A27, Lm3, ZFMISC_1:87;
consider x99, s99 being Element of REAL+  such that
A29: r = [0,x99] and
A30: s = [0,s99] and
A31: s99 <=' x99 by A1, A23, A24, XXREAL_0:def_5;
A32: s9 = s99 by A30, A25, XTUPLE_0:1;
consider x9, t9 being Element of REAL+  such that
A33: r = [0,x9] and
A34: t = t9 and
A35: * (x1,z1) = [0,(t9 *' x9)] by A3, A13, A23, ARYTM_0:def_2;
A36: * (x1,z1) in [:{0},REAL+:] by A35, Lm3, ZFMISC_1:87;
 x9 = x99 by A29, A33, XTUPLE_0:1;
then  s9 *' t9 <=' x9 *' t9 by A31, A32, ARYTM_1:8;
hence  contradiction by A11, A12, A34, A35, A26, A27, A36, A28, Lm2; ::_thesis: verum
end;
end;
end;

Lm17:  for r, s being real number st r > 0 & s > 0 holds
r * s > 0
proof
let r, s be real number ; ::_thesis: ( r > 0 & s > 0 implies r * s > 0 )
assume A1: ( r > 0 & s > 0 ) ; ::_thesis: r * s > 0
then  r * s >= 0 * s by Lm16;
hence  r * s > 0 by A1, Lm4; ::_thesis: verum
end;

Lm18:  for r, s being real number st r > 0 & s < 0 holds
r * s < 0
proof
let r, s be real number ; ::_thesis: ( r > 0 & s < 0 implies r * s < 0 )
assume A1: ( r > 0 & s < 0 ) ; ::_thesis: r * s < 0
then  r * s <= r * 0 by Lm16;
hence  r * s < 0 by A1, Lm4; ::_thesis: verum
end;

Lm19:  for s, t being real number st s <= t holds
- t <= - s
proof
let s, t be real number ; ::_thesis: ( s <= t implies - t <= - s )
assume  s <= t ; ::_thesis: - t <= - s
then  s - t <= t - t by Lm5;
then  (s - t) - s <= 0 - s by Lm5;
hence  - t <= - s ; ::_thesis: verum
end;

Lm20:  for r, s being real number st r <= 0 & s >= 0 holds
r * s <= 0
proof
let r, s be real number ; ::_thesis: ( r <= 0 & s >= 0 implies r * s <= 0 )
assume A1: ( r <= 0 & s >= 0 ) ; ::_thesis: r * s <= 0
percases ( r = 0 or s = 0 or ( r < 0 & s > 0 ) ) by A1, Lm4;
suppose ( r = 0 or s = 0 ) ; ::_thesis: r * s <= 0
hence  r * s <= 0 ; ::_thesis: verum
end;
suppose ( r < 0 & s > 0 ) ; ::_thesis: r * s <= 0
hence  r * s <= 0 by Lm18; ::_thesis: verum
end;
end;
end;

registration
cluster complex ext-real positive real for set ;
existence
 ex b1 being real number st b1 is positive
proof
take r = 1; ::_thesis: r is positive
thus  0 < r by Lm4, Lm8; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
cluster complex ext-real negative real for set ;
existence
 ex b1 being real number st b1 is negative
proof
take r = - 1; ::_thesis: r is negative
thus  0 > r by Lm7, Lm13, XXREAL_0:def_5; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
cluster zero complex ext-real real for set ;
existence
 ex b1 being real number st b1 is zero
proof
take  0 ; ::_thesis: 0 is zero
thus  0 is zero ; ::_thesis: verum
end;
end;

registration
let r, s be non negative real number ;
clusterr + s ->  non negative ;
coherence
 not r + s is negative
proof
A1: s >= 0 by XXREAL_0:def_7;
A2: r >= 0 by XXREAL_0:def_7;
percases ( r = 0 or r > 0 ) by A2, Lm4;
suppose r = 0 ; ::_thesis: not r + s is negative
hence  r + s >= 0 by XXREAL_0:def_7; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
suppose r > 0 ; ::_thesis: not r + s is negative
hence  r + s >= 0 by A1, Lm14; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;

registration
let r, s be non positive real number ;
clusterr + s ->  non positive ;
coherence
 not r + s is positive
proof
A1: s <= 0 by XXREAL_0:def_6;
A2: r <= 0 by XXREAL_0:def_6;
percases ( r = 0 or r < 0 ) by A2, Lm4;
suppose r = 0 ; ::_thesis: not r + s is positive
hence  r + s <= 0 by XXREAL_0:def_6; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
suppose r < 0 ; ::_thesis: not r + s is positive
hence  r + s <= 0 by A1, Lm15; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
end;
end;
end;

registration
let r be positive real number ;
let s be non negative real number ;
clusterr + s ->  positive ;
coherence
 r + s is positive
proof
 ( r > 0 & s >= 0 ) by XXREAL_0:def_6;
hence  r + s > 0 by Lm14; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
clusters + r ->  positive ;
coherence
 s + r is positive ;
end;

registration
let r be negative real number ;
let s be non positive real number ;
clusterr + s ->  negative ;
coherence
 r + s is negative
proof
 ( r < 0 & s <= 0 ) by XXREAL_0:def_7;
hence  r + s < 0 by Lm15; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
clusters + r ->  negative ;
coherence
 s + r is negative ;
end;

registration
let r be non positive real number ;
cluster - r ->  non negative ;
coherence
 not - r is negative
proof
assume A1: - r < 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction
 - (- r) <= 0 by XXREAL_0:def_6;
then  (- r) + (- (- r)) < 0 by A1, Lm15;
hence  contradiction ; ::_thesis: verum
end;
end;

registration
let r be non negative real number ;
cluster - r ->  non positive ;
coherence
 not - r is positive
proof
assume A1: - r > 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction
 - (- r) >= 0 by XXREAL_0:def_7;
then  (- r) + (- (- r)) > 0 by A1, Lm14;
hence  contradiction ; ::_thesis: verum
end;
end;

registration
let r be non negative real number ;
let s be non positive real number ;
clusterr - s ->  non negative ;
coherence
 not r - s is negative ;
clusters - r ->  non positive ;
coherence
 not s - r is positive ;
end;

registration
let r be positive real number ;
let s be non positive real number ;
clusterr - s ->  positive ;
coherence
 r - s is positive ;
clusters - r ->  negative ;
coherence
 s - r is negative ;
end;

registration
let r be negative real number ;
let s be non negative real number ;
clusterr - s ->  negative ;
coherence
 r - s is negative ;
clusters - r ->  positive ;
coherence
 s - r is positive ;
end;

registration
let r be non positive real number ;
let s be non negative real number ;
clusterr * s ->  non positive ;
coherence
 not r * s is positive
proof
 ( r <= 0 & s >= 0 ) by XXREAL_0:def_6;
hence  r * s <= 0 by Lm20; :: according to XXREAL_0:def_6 ::_thesis: verum
end;
clusters * r ->  non positive ;
coherence
 not s * r is positive ;
end;

registration
let r, s be non positive real number ;
clusterr * s ->  non negative ;
coherence
 not r * s is negative
proof
A1: ( r <= 0 & s <= 0 ) by XXREAL_0:def_6;
percases ( r = 0 or s = 0 or ( - (- r) < - (- 0) & s < 0 ) ) by A1, Lm4;
suppose ( r = 0 or s = 0 ) ; ::_thesis: not r * s is negative
hence  r * s >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
supposeA2: ( - (- r) < - (- 0) & s < 0 ) ; ::_thesis: not r * s is negative
then  0 < - r by Lm19;
then  s * (- r) <= 0 * (- r) by A2, Lm16;
then  s * (- r) < 0 * (- r) by A2, Lm4;
then  - (- (0 * r)) < - (- (s * r)) by Lm19;
hence  r * s >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;

registration
let r, s be non negative real number ;
clusterr * s ->  non negative ;
coherence
 not r * s is negative
proof
A1: ( r >= 0 & s >= 0 ) by XXREAL_0:def_7;
percases ( r = 0 or s = 0 or ( r > 0 & s > 0 ) ) by A1, Lm4;
suppose ( r = 0 or s = 0 ) ; ::_thesis: not r * s is negative
hence  r * s >= 0 ; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
suppose ( r > 0 & s > 0 ) ; ::_thesis: not r * s is negative
hence  r * s >= 0 by Lm17; :: according to XXREAL_0:def_7 ::_thesis: verum
end;
end;
end;
end;

registration
let r be positive real number ;
clusterr "  ->  positive ;
coherence
 r " is positive
proof
assume A1: r " <= 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction
 (r ") " > 0 by XXREAL_0:def_6;
then  ( (r ") * ((r ") ") = 1 & (r ") * ((r ") ") <= 0 ) by A1, Lm20, XCMPLX_0:def_7;
hence  contradiction by Lm4, Lm8; ::_thesis: verum
end;
end;

registration
let r be non positive real number ;
clusterr "  ->  non positive ;
coherence
 not r " is positive
proof
A1: (r ") " <= 0 by XXREAL_0:def_6;
assume A2: r " > 0 ; :: according to XXREAL_0:def_6 ::_thesis: contradiction
percases ( (r ") " = 0 or (r ") " < 0 ) by A1, Lm4;
suppose (r ") " = 0 ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;
supposeA3: (r ") " < 0 ; ::_thesis: contradiction
 (r ") * ((r ") ") = 1 by A2, XCMPLX_0:def_7;
hence  contradiction by A2, A3, Lm8, Lm18; ::_thesis: verum
end;
end;
end;
end;

registration
let r be negative real number ;
clusterr "  ->  negative ;
coherence
 r " is negative ;
end;

registration
let r be non negative real number ;
clusterr "  ->  non negative ;
coherence
 not r " is negative
proof
A1: (r ") " >= 0 by XXREAL_0:def_7;
assume A2: r " < 0 ; :: according to XXREAL_0:def_7 ::_thesis: contradiction
percases ( (r ") " = 0 or (r ") " > 0 ) by A1, Lm4;
suppose (r ") " = 0 ; ::_thesis: contradiction
hence  contradiction by A2; ::_thesis: verum
end;
supposeA3: (r ") " > 0 ; ::_thesis: contradiction
 (r ") * ((r ") ") = 1 by A2, XCMPLX_0:def_7;
hence  contradiction by A2, A3, Lm8, Lm18; ::_thesis: verum
end;
end;
end;
end;

registration
let r be non negative real number ;
let s be non positive real number ;
clusterr / s ->  non positive ;
coherence
 not r / s is positive ;
clusters / r ->  non positive ;
coherence
 not s / r is positive ;
end;

registration
let r, s be non negative real number ;
clusterr / s ->  non negative ;
coherence
 not r / s is negative ;
end;

registration
let r, s be non positive real number ;
clusterr / s ->  non negative ;
coherence
 not r / s is negative ;
end;

begin

registration
let r, s be real number ;
cluster min (r,s) ->  real ;
coherence
 min (r,s) is real by XXREAL_0:15;
cluster max (r,s) ->  real ;
coherence
 max (r,s) is real by XXREAL_0:16;
end;

definition
let r, s be real number ;
funcr -' s ->  set  equals :Def2: :: XREAL_0:def 2
r - s if r - s >= 0
otherwise  0 ;
correctness
coherence
( ( r - s >= 0 implies r - s is set ) & ( not r - s >= 0 implies 0 is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def2 defines -' XREAL_0:def_2_:_
 for r, s being real number holds
( ( r - s >= 0 implies r -' s = r - s ) & ( not r - s >= 0 implies r -' s = 0 ) );

registration
let r, s be real number ;
clusterr -' s ->  real ;
coherence
 r -' s is real
proof
 ( r -' s = r - s or r -' s = 0 ) by Def2;
hence  r -' s is real ; ::_thesis: verum
end;
end;

registration
let r, s be real number ;
clusterr -' s ->  non negative real for real number ;
coherence
 for b1 being real number st b1 = r -' s holds
not b1 is negative
proof
 ( ( r -' s = r - s & r - s >= 0 ) or r -' s = 0 ) by Def2;
hence  for b1 being real number st b1 = r -' s holds
not b1 is negative by XXREAL_0:def_7; ::_thesis: verum
end;
end;