let x, y, z be R_eal; :: thesis: ( not x = -infty & not x = +infty implies ( y + x <= z iff y <= z - x ) )
assume A1: ( not x = -infty & not x = +infty ) ; :: thesis: ( y + x <= z iff y <= z - x )
A2: ( ( x in REAL or x in {-infty ,+infty } ) & ( y in REAL or y in {-infty ,+infty } ) & ( z in REAL or z in {-infty ,+infty } ) ) by XBOOLE_0:def 3, XXREAL_0:def 4;

hereby :: thesis: ( y <= z - x implies y + x <= z )

assume A3: y + x <= z ; :: thesis: y <= z - x
(y + x) - x = y

proof

per cases ( y in REAL or y = -infty or y = +infty ) by A2, TARSKI:def 2;

suppose y in REAL ; :: thesis: (y + x) - x = y

then consider a, b being Real such that
A4: ( a = x & b = y ) by A1, A2, TARSKI:def 2;
y + x = b + a by A4, SUPINF_2:1;
then consider c being Real such that
A5: c = y + x ;
(y + x) - x = c - a by A4, A5, SUPINF_2:5
.= (b + a) - a by A4, A5, SUPINF_2:1
.= y by A4 ;
hence (y + x) - x = y ; :: thesis: verum

end;

suppose A6: ( y = -infty or y = +infty ) ; :: thesis: (y + x) - x = y

now

per cases ( y = -infty or y = +infty ) by A6;

suppose A7: y = -infty ; :: thesis: (y + x) - x = y

hence (y + x) - x = -infty - x by A1, SUPINF_2:def 2
.= y by A1, A7, SUPINF_2:7 ;
:: thesis: verum

end;

suppose A8: y = +infty ; :: thesis: (y + x) - x = y

hence (y + x) - x = +infty - x by A1, SUPINF_2:def 2
.= y by A1, A8, SUPINF_2:6 ;
:: thesis: verum

end;

end;

end;

hence (y + x) - x = y ; :: thesis: verum

end;

end;

end;

hence y <= z - x by A3, SUPINF_2:15; :: thesis: verum

end;

assume A9: y <= z - x ; :: thesis: y + x <= z
(z - x) + x = z

proof

per cases ( z in REAL or z = -infty or z = +infty ) by A2, TARSKI:def 2;

suppose z in REAL ; :: thesis: (z - x) + x = z

then consider a, b being Real such that
A10: ( a = x & b = z ) by A1, A2, TARSKI:def 2;
z - x = b - a by A10, SUPINF_2:5;
then consider c being Real such that
A11: c = z - x ;
thus (z - x) + x = c + a by A10, A11, SUPINF_2:1
.= (b - a) + a by A10, A11, SUPINF_2:5
.= z by A10 ; :: thesis: verum

end;

suppose A12: z = -infty ; :: thesis: (z - x) + x = z

hence (z - x) + x = -infty + x by A1, SUPINF_2:7
.= z by A1, A12, SUPINF_2:def 2 ;
:: thesis: verum

end;

suppose A13: z = +infty ; :: thesis: (z - x) + x = z

hence (z - x) + x = +infty + x by A1, SUPINF_2:6
.= z by A1, A13, SUPINF_2:def 2 ;
:: thesis: verum

end;

end;

end;

hence y + x <= z by A9, SUPINF_2:14; :: thesis: verum