let a, b, c be R_eal; :: thesis: ( b <> -infty & b <> +infty & ( not a = -infty or not c = -infty ) & ( not a = +infty or not c = +infty ) implies (c - b) + (b - a) = c - a )
assume A1: ( b <> -infty & b <> +infty & ( not a = -infty or not c = -infty ) & ( not a = +infty or not c = +infty ) ) ; :: thesis: (c - b) + (b - a) = c - a
A2: ( ( a in REAL or a in {-infty ,+infty } ) & ( b in REAL or b in {-infty ,+infty } ) ) by XBOOLE_0:def 3, XXREAL_0:def 4;

per cases ( ( a in REAL & b in REAL ) or ( a = -infty & b in REAL ) or ( a = +infty & b in REAL ) ) by A1, A2, TARSKI:def 2;

suppose A3: ( a in REAL & b in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

A4: ( c in REAL or c in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

now

per cases ( ( a in REAL & b in REAL & c in REAL ) or ( a in REAL & b in REAL & c = -infty ) or ( a in REAL & b in REAL & c = +infty ) ) by A3, A4, TARSKI:def 2;

suppose ( a in REAL & b in REAL & c in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

then consider x, y, z being Real such that
A5: ( x = a & y = b & z = c ) ;
( c - b = z - y & b - a = y - x ) by A5, SUPINF_2:5;
hence (c - b) + (b - a) = (z - y) + (y - x) by SUPINF_2:1
.= z - (0 + x)
.= c - a by A5, SUPINF_2:5 ;
:: thesis: verum

end;

suppose A6: ( a in REAL & b in REAL & c = -infty ) ; :: thesis: (c - b) + (b - a) = c - a

then A7: (c - b) + (b - a) = -infty + (b - a) by SUPINF_2:7;
consider x, y being Real such that
A8: ( x = a & y = b ) by A6;
b - a = y - x by A8, SUPINF_2:5;
then (c - b) + (b - a) = -infty by A7, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A6, SUPINF_2:7; :: thesis: verum

end;

suppose A9: ( a in REAL & b in REAL & c = +infty ) ; :: thesis: (c - b) + (b - a) = c - a

then A10: (c - b) + (b - a) = +infty + (b - a) by SUPINF_2:6;
consider x, y being Real such that
A11: ( x = a & y = b ) by A9;
b - a = y - x by A11, SUPINF_2:5;
then (c - b) + (b - a) = +infty by A10, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A9, SUPINF_2:6; :: thesis: verum

end;

end;

end;

hence (c - b) + (b - a) = c - a ; :: thesis: verum

end;

suppose A12: ( a = -infty & b in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

A13: ( c in REAL or c in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

now

per cases ( ( a = -infty & b in REAL & c in REAL ) or ( a = -infty & b in REAL & c = +infty ) ) by A1, A12, A13, TARSKI:def 2;

suppose A14: ( a = -infty & b in REAL & c in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

then A15: (c - b) + (b - a) = (c - b) + +infty by SUPINF_2:7;
consider x, y being Real such that
A16: ( x = c & y = b ) by A14;
c - b = x - y by A16, SUPINF_2:5;
then (c - b) + (b - a) = +infty by A15, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A14, SUPINF_2:7; :: thesis: verum

end;

suppose A17: ( a = -infty & b in REAL & c = +infty ) ; :: thesis: (c - b) + (b - a) = c - a

then A18: (c - b) + (b - a) = (c - b) + +infty by SUPINF_2:7;
c - b = +infty by A17, SUPINF_2:6;
then (c - b) + (b - a) = +infty by A18, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A17, SUPINF_2:7; :: thesis: verum

end;

end;

end;

hence (c - b) + (b - a) = c - a ; :: thesis: verum

end;

suppose A19: ( a = +infty & b in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

A20: ( c in REAL or c in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

now

per cases ( ( a = +infty & b in REAL & c in REAL ) or ( a = +infty & b in REAL & c = -infty ) ) by A1, A19, A20, TARSKI:def 2;

suppose A21: ( a = +infty & b in REAL & c in REAL ) ; :: thesis: (c - b) + (b - a) = c - a

then A22: (c - b) + (b - a) = (c - b) + -infty by SUPINF_2:6;
consider x, y being Real such that
A23: ( x = c & y = b ) by A21;
c - b = x - y by A23, SUPINF_2:5;
then (c - b) + (b - a) = -infty by A22, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A21, SUPINF_2:6; :: thesis: verum

end;

suppose A24: ( a = +infty & b in REAL & c = -infty ) ; :: thesis: (c - b) + (b - a) = c - a

then A25: (c - b) + (b - a) = (c - b) + -infty by SUPINF_2:6;
c - b = -infty by A24, SUPINF_2:7;
then (c - b) + (b - a) = -infty by A25, SUPINF_2:def 2;
hence (c - b) + (b - a) = c - a by A24, SUPINF_2:6; :: thesis: verum

end;

end;

end;

hence (c - b) + (b - a) = c - a ; :: thesis: verum

end;

end;