let r, s, t be Real; :: 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 st x9 = r holds
+ (x9,z1) = r + t

proof

let x9 be Element of REAL ; :: thesis: for r being Real st x9 = r holds
+ (x9,z1) = r + t
let r be Real; :: 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

per cases ( ( 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;

suppose that 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;

suppose that 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

per cases ( x9 <=' t9 or not x9 <=' t9 ) ;

suppose A23: 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;

suppose that 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

per cases ( x9 <=' t9 or not x9 <=' t9 ) ;

suppose A40: 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

per cases ( 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;

suppose A46: 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;

suppose that 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

per cases ( t9 <=' x9 or not t9 <=' x9 ) ;

suppose A60: 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

per cases ( 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;

suppose A66: 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;

suppose that 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

per cases ( 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;

suppose A79: 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;

suppose that 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;