let x, y, z be ExtReal; :: thesis: ( x is real implies ( y + x <= z iff y <= z - x ) )
assume A1: x is real ; :: thesis: ( y + x <= z iff y <= z - x )
A2: (z - x) + x = z

proof

per cases ( z in REAL or z = -infty or z = +infty ) by XXREAL_0:14;

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

then reconsider a = x, b = z as Real by A1;
thus (z - x) + x = (b - a) + a
.= z ; :: thesis: verum

end;

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

hence (z - x) + x = -infty + x by A1, Th14
.= z by A1, A3, Def2 ;
:: thesis: verum

end;

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

hence (z - x) + x = +infty + x by A1, Th13
.= z by A1, A4, Def2 ;
:: thesis: verum

end;

end;

end;

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

A5: (y + x) - x = y

proof

per cases ( y in REAL or y = -infty or y = +infty ) by XXREAL_0:14;

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

then reconsider a = x, b = y as Element of REAL by A1, XXREAL_0:14;
(y + x) - x = (b + a) - a
.= y ;
hence (y + x) - x = y ; :: thesis: verum

end;

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

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, Def2
.= y by A1, A7, Th14 ;
:: thesis: verum

end;

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

hence (y + x) - x = +infty - x by A1, Def2
.= y by A1, A8, Th13 ;
:: thesis: verum

end;

end;

end;

end;

end;

assume y + x <= z ; :: thesis: y <= z - x
hence y <= z - x by A5, Th37; :: thesis: verum

end;

assume y <= z - x ; :: thesis: y + x <= z
hence y + x <= z by A2, Th36; :: thesis: verum