let x, y, z be R_eal; :: thesis: ( 0. <= y & 0. <= z & x = y + z & y < +infty implies z = x - y )
assume A1: ( 0. <= y & 0. <= z & x = y + z & y < +infty ) ; :: thesis: z = x - y
then 0. + 0. <= y + z by Th4;
then A2: 0 <= x by A1, SUPINF_2:18;
(y + z) - y = z

proof

A3: ( not x = -infty & not y = -infty & not z = -infty ) by A1, A2, XXREAL_0:12;
A4: ( ( x in REAL or x in {-infty ,+infty } ) & ( y in REAL or y in {-infty ,+infty } ) ) by XBOOLE_0:def 3, XXREAL_0:def 4;
A5: ( x in REAL & y in REAL implies (y + z) - y = z )

proof

assume ( x in REAL & y in REAL ) ; :: thesis: (y + z) - y = z
then reconsider a = y, b = z as Real by A1, A3, SUPINF_2:12;
y + z = a + b by SUPINF_2:1;
then (y + z) - y = (a + b) - a by SUPINF_2:5
.= z ;
hence (y + z) - y = z ; :: thesis: verum

end;

( x = +infty & y in REAL implies (y + z) - y = z )

proof

assume A6: ( x = +infty & y in REAL ) ; :: thesis: (y + z) - y = z
then (y + z) - y = +infty by A1, SUPINF_2:6
.= z by A1, A6, SUPINF_2:8 ;
hence (y + z) - y = z ; :: thesis: verum

end;

hence (y + z) - y = z by A1, A3, A4, A5, TARSKI:def 2; :: thesis: verum

end;

hence z = x - y by A1; :: thesis: verum