let a, b, c be real number ; :: thesis: ( a <= b implies a + c <= b + c )
reconsider x1 = a, y1 = b, z1 = c as Element of REAL by XREAL_0:def 1;
A1: + y1,z1 = b + c by Lm3;
A2: + x1,z1 = a + c by Lm3;
assume A3: a <= b ; :: thesis: a + c <= b + c

per cases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in [:{0 },REAL+ :] & b in REAL+ & c in REAL+ ) or ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] & c in REAL+ ) or ( a in REAL+ & b in REAL+ & c in [:{0 },REAL+ :] ) or ( a in [:{0 },REAL+ :] & b in REAL+ & c in [:{0 },REAL+ :] ) or ( a in [:{0 },REAL+ :] & b in [:{0 },REAL+ :] & c in [:{0 },REAL+ :] ) ) by A3, XXREAL_0:def 5;

suppose that A4: a in REAL+ and
A5: b in REAL+ and
A6: c in REAL+ ; :: thesis: a + c <= b + c

consider b', c'' being Element of REAL+ such that
A7: b = b' and
A8: c = c'' and
A9: + y1,z1 = b' + c'' by A5, A6, ARYTM_0:def 2;
consider a', c' being Element of REAL+ such that
A10: a = a' and
A11: c = c' and
A12: + x1,z1 = a' + c' by A4, A6, ARYTM_0:def 2;
ex a'', b'' being Element of REAL+ st
( a = a'' & b = b'' & a'' <=' b'' ) by A3, A4, A5, XXREAL_0:def 5;
then a' + c' <=' b' + c'' by A10, A11, A7, A8, ARYTM_1:7;
hence a + c <= b + c by A1, A2, A12, A9, Lm1; :: thesis: verum

end;

suppose that A13: a in [:{0 },REAL+ :] and
A14: b in REAL+ and
A15: c in REAL+ ; :: thesis: a + c <= b + c

consider b', c'' being Element of REAL+ such that
b = b' and
A16: c = c'' and
A17: + y1,z1 = b' + c'' by A14, A15, ARYTM_0:def 2;
consider a', c' being Element of REAL+ such that
a = [0 ,a'] and
A18: c = c' and
A19: + x1,z1 = c' - a' by A13, A15, ARYTM_0:def 2;

now

per cases ( a' <=' c' or not a' <=' c' ) ;

suppose A20: a' <=' c' ; :: thesis: a + c <= b + c

A21: c' -' a' <=' c' by ARYTM_1:11;
c' <=' b' + c'' by A18, A16, ARYTM_2:20;
then A22: c' -' a' <=' b' + c'' by A21, ARYTM_1:3;
c' - a' = c' -' a' by A20, ARYTM_1:def 2;
hence a + c <= b + c by A1, A2, A19, A17, A22, Lm1; :: thesis: verum

end;

suppose not a' <=' c' ; :: thesis: a + c <= b + c

then c' - a' = [0 ,(a' -' c')] by ARYTM_1:def 2;
then c' - a' in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
then A23: not a + c in REAL+ by A2, A19, ARYTM_0:5, XBOOLE_0:3;
not b + c in [:{0 },REAL+ :] by A1, A17, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A23, XXREAL_0:def 5; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

suppose that A24: a in [:{0 },REAL+ :] and
A25: b in [:{0 },REAL+ :] and
A26: c in REAL+ ; :: thesis: a + c <= b + c

consider b', c'' being Element of REAL+ such that
A27: b = [0 ,b'] and
A28: c = c'' and
A29: + y1,z1 = c'' - b' by A25, A26, ARYTM_0:def 2;
consider a'', b'' being Element of REAL+ such that
A30: a = [0 ,a''] and
A31: b = [0 ,b''] and
A32: b'' <=' a'' by A3, A24, A25, XXREAL_0:def 5;
consider a', c' being Element of REAL+ such that
A33: a = [0 ,a'] and
A34: c = c' and
A35: + x1,z1 = c' - a' by A24, A26, ARYTM_0:def 2;
A36: a' = a'' by A30, A33, ZFMISC_1:33;
A37: b' = b'' by A31, A27, ZFMISC_1:33;

now

per cases ( a' <=' c' or not a' <=' c' ) ;

suppose A38: a' <=' c' ; :: thesis: a + c <= b + c

then b' <=' c' by A32, A36, A37, ARYTM_1:3;
then A39: c' - b' = c' -' b' by ARYTM_1:def 2;
A40: c' - a' = c' -' a' by A38, ARYTM_1:def 2;
c' -' a' <=' c'' -' b' by A32, A34, A28, A36, A37, ARYTM_1:16;
hence a + c <= b + c by A1, A2, A34, A35, A28, A29, A40, A39, Lm1; :: thesis: verum

end;

suppose not a' <=' c' ; :: thesis: a + c <= b + c

then A41: + x1,z1 = [0 ,(a' -' c')] by A35, ARYTM_1:def 2;
then A42: + x1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;

now

per cases ( b' <=' c' or not b' <=' c' ) ;

suppose b' <=' c' ; :: thesis: a + c <= b + c

then c' - b' = c' -' b' by ARYTM_1:def 2;
then A43: not + y1,z1 in [:{0 },REAL+ :] by A34, A28, A29, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A42, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A1, A2, A43, XXREAL_0:def 5; :: thesis: verum

end;

suppose A44: not b' <=' c' ; :: thesis: a + c <= b + c

A45: b' -' c' <=' a' -' c' by A32, A36, A37, ARYTM_1:17;
A46: + y1,z1 = [0 ,(b' -' c')] by A34, A28, A29, A44, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
hence a + c <= b + c by A1, A2, A41, A42, A46, A45, Lm1; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

suppose that A47: a in REAL+ and
A48: b in REAL+ and
A49: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

consider b', c'' being Element of REAL+ such that
A50: b = b' and
A51: c = [0 ,c''] and
A52: + y1,z1 = b' - c'' by A48, A49, ARYTM_0:def 2;
consider a', c' being Element of REAL+ such that
A53: a = a' and
A54: c = [0 ,c'] and
A55: + x1,z1 = a' - c' by A47, A49, ARYTM_0:def 2;
A56: c' = c'' by A54, A51, ZFMISC_1:33;
A57: ex a'', b'' being Element of REAL+ st
( a = a'' & b = b'' & a'' <=' b'' ) by A3, A47, A48, XXREAL_0:def 5;

now

per cases ( c' <=' a' or not c' <=' a' ) ;

suppose A58: c' <=' a' ; :: thesis: a + c <= b + c

then c' <=' b' by A57, A53, A50, ARYTM_1:3;
then A59: b' - c' = b' -' c' by ARYTM_1:def 2;
A60: a' - c' = a' -' c' by A58, ARYTM_1:def 2;
a' -' c' <=' b' -' c'' by A57, A53, A50, A56, ARYTM_1:17;
hence a + c <= b + c by A1, A2, A55, A52, A56, A60, A59, Lm1; :: thesis: verum

end;

suppose not c' <=' a' ; :: thesis: a + c <= b + c

then A61: + x1,z1 = [0 ,(c' -' a')] by A55, ARYTM_1:def 2;
then A62: + x1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;

now

per cases ( c' <=' b' or not c' <=' b' ) ;

suppose c' <=' b' ; :: thesis: a + c <= b + c

then b' - c' = b' -' c' by ARYTM_1:def 2;
then A63: not + y1,z1 in [:{0 },REAL+ :] by A52, A56, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A62, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A1, A2, A63, XXREAL_0:def 5; :: thesis: verum

end;

suppose A64: not c' <=' b' ; :: thesis: a + c <= b + c

A65: c' -' b' <=' c' -' a' by A57, A53, A50, ARYTM_1:16;
A66: + y1,z1 = [0 ,(c' -' b')] by A52, A56, A64, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
hence a + c <= b + c by A1, A2, A61, A62, A66, A65, Lm1; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

suppose that A67: a in [:{0 },REAL+ :] and
A68: b in REAL+ and
A69: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

A70: not c in REAL+ by A69, ARYTM_0:5, XBOOLE_0:3;
not a in REAL+ by A67, ARYTM_0:5, XBOOLE_0:3;
then consider a', c' being Element of REAL+ such that
a = [0 ,a'] and
A71: c = [0 ,c'] and
A72: + x1,z1 = [0 ,(a' + c')] by A70, ARYTM_0:def 2;
A73: + x1,z1 in [:{0 },REAL+ :] by A72, Lm4, ZFMISC_1:106;
consider b', c'' being Element of REAL+ such that
b = b' and
A74: c = [0 ,c''] and
A75: + y1,z1 = b' - c'' by A68, A69, ARYTM_0:def 2;
A76: c' = c'' by A71, A74, ZFMISC_1:33;

now

per cases ( c' <=' b' or not c' <=' b' ) ;

suppose c' <=' b' ; :: thesis: a + c <= b + c

then b' - c'' = b' -' c'' by A76, ARYTM_1:def 2;
then A77: not + y1,z1 in [:{0 },REAL+ :] by A75, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A73, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A1, A2, A77, XXREAL_0:def 5; :: thesis: verum

end;

suppose A78: not c' <=' b' ; :: thesis: a + c <= b + c

A79: c' <=' c' + a' by ARYTM_2:20;
c' -' b' <=' c' by ARYTM_1:11;
then A80: c' -' b' <=' c' + a' by A79, ARYTM_1:3;
A81: + y1,z1 = [0 ,(c' -' b')] by A75, A76, A78, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
hence a + c <= b + c by A1, A2, A72, A73, A81, A80, Lm1; :: thesis: verum

end;

end;

end;

hence a + c <= b + c ; :: thesis: verum

end;

suppose that A82: a in [:{0 },REAL+ :] and
A83: b in [:{0 },REAL+ :] and
A84: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

A85: not c in REAL+ by A84, ARYTM_0:5, XBOOLE_0:3;
A86: not c in REAL+ by A84, ARYTM_0:5, XBOOLE_0:3;
not a in REAL+ by A82, ARYTM_0:5, XBOOLE_0:3;
then consider a', c' being Element of REAL+ such that
A87: a = [0 ,a'] and
A88: c = [0 ,c'] and
A89: + x1,z1 = [0 ,(a' + c')] by A86, ARYTM_0:def 2;
A90: + x1,z1 in [:{0 },REAL+ :] by A89, Lm4, ZFMISC_1:106;
not b in REAL+ by A83, ARYTM_0:5, XBOOLE_0:3;
then consider b', c'' being Element of REAL+ such that
A91: b = [0 ,b'] and
A92: c = [0 ,c''] and
A93: + y1,z1 = [0 ,(b' + c'')] by A85, ARYTM_0:def 2;
A94: + y1,z1 in [:{0 },REAL+ :] by A93, Lm4, ZFMISC_1:106;
A95: c' = c'' by A88, A92, ZFMISC_1:33;
consider a'', b'' being Element of REAL+ such that
A96: a = [0 ,a''] and
A97: b = [0 ,b''] and
A98: b'' <=' a'' by A3, A82, A83, XXREAL_0:def 5;
A99: b' = b'' by A97, A91, ZFMISC_1:33;
a' = a'' by A96, A87, ZFMISC_1:33;
then b' + c' <=' a' + c'' by A98, A99, A95, ARYTM_1:7;
hence a + c <= b + c by A1, A2, A89, A93, A95, A90, A94, Lm1; :: thesis: verum

end;

end;