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

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 A1, XXREAL_0:def 5;

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

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

end;

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

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

now

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

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

then A22: c' - a' = c' -' a' by ARYTM_1:def 2;
A23: c' -' a' <=' c' by ARYTM_1:11;
c' <=' b' + c'' by A18, A20, ARYTM_2:20;
then c' -' a' <=' b' + c'' by A23, ARYTM_1:3;
hence a + c <= b + c by A2, A19, A21, 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 ( not a + c in REAL+ & not b + c in [:{0 },REAL+ :] ) by A2, A19, A21, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by 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 a'', b'' being Element of REAL+ such that
A27: a = [0 ,a''] and
A28: b = [0 ,b''] and
A29: b'' <=' a'' by A1, A24, A25, XXREAL_0:def 5;
consider a', c' being Element of REAL+ such that
A30: a = [0 ,a'] and
A31: c = c' and
A32: + x1,z1 = c' - a' by A24, A26, ARYTM_0:def 2;
consider b', c'' being Element of REAL+ such that
A33: b = [0 ,b'] and
A34: c = c'' and
A35: + y1,z1 = c'' - b' by A25, A26, ARYTM_0:def 2;
A36: a' = a'' by A27, A30, ZFMISC_1:33;
A37: b' = b'' by A28, A33, ZFMISC_1:33;

now

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

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

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

end;

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

then A41: + x1,z1 = [0 ,(a' -' c')] by A32, 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 ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A31, A34, A35, A42, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A2, XXREAL_0:def 5; :: thesis: verum

end;

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

then A43: + y1,z1 = [0 ,(b' -' c')] by A31, A34, A35, ARYTM_1:def 2;
then A44: + y1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
b' -' c' <=' a' -' c' by A29, A36, A37, ARYTM_1:17;
hence a + c <= b + c by A2, A41, A42, A43, A44, 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 A45: a in REAL+ and
A46: b in REAL+ and
A47: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

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

now

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

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

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

end;

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

then A61: + x1,z1 = [0 ,(c' -' a')] by A53, 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 ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A56, A57, A62, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A2, XXREAL_0:def 5; :: thesis: verum

end;

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

then A63: + y1,z1 = [0 ,(c' -' b')] by A56, A57, ARYTM_1:def 2;
then A64: + y1,z1 in [:{0 },REAL+ :] by Lm4, ZFMISC_1:106;
c' -' b' <=' c' -' a' by A48, A49, A50, A51, A54, ARYTM_1:16;
hence a + c <= b + c by A2, A61, A62, A63, A64, 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 A65: a in [:{0 },REAL+ :] and
A66: b in REAL+ and
A67: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

( not a in REAL+ & not c in REAL+ ) by A65, A67, ARYTM_0:5, XBOOLE_0:3;
then consider a', c' being Element of REAL+ such that
a = [0 ,a'] and
A68: c = [0 ,c'] and
A69: + x1,z1 = [0 ,(a' + c')] by ARYTM_0:def 2;
consider b', c'' being Element of REAL+ such that
b = b' and
A70: c = [0 ,c''] and
A71: + y1,z1 = b' - c'' by A66, A67, ARYTM_0:def 2;
A72: c' = c'' by A68, A70, ZFMISC_1:33;
A73: + x1,z1 in [:{0 },REAL+ :] by A69, 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 A72, ARYTM_1:def 2;
then ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A71, A73, ARYTM_0:5, XBOOLE_0:3;
hence a + c <= b + c by A2, XXREAL_0:def 5; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

suppose that A77: a in [:{0 },REAL+ :] and
A78: b in [:{0 },REAL+ :] and
A79: c in [:{0 },REAL+ :] ; :: thesis: a + c <= b + c

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

end;

end;