let x, z be R_eal; :: thesis: ( 0. <= x & x < z implies ex y being R_eal st
( 0. < y & x + y < z & y in REAL ) )
assume A1: ( 0. <= x & x < z ) ; :: thesis: ex y being R_eal st
( 0. < y & x + y < z & y in REAL )

per cases ( 0. < x or 0. = x ) by A1, XXREAL_0:1;

suppose 0. < x ; :: thesis: ex y being R_eal st
( 0. < y & x + y < z & y in REAL )

hence ex y being R_eal st
( 0. < y & x + y < z & y in REAL ) by A1, Th24; :: thesis: verum

end;

suppose A2: 0. = x ; :: thesis: ex y being R_eal st
( 0. < y & x + y < z & y in REAL )

then consider y being R_eal such that
A3: ( 0. < y & y < z ) by A1, Th23;
take y ; :: thesis: ( 0. < y & x + y < z & y in REAL )
y is Real by A3, XXREAL_0:48;
hence ( 0. < y & x + y < z & y in REAL ) by A2, A3, SUPINF_2:18; :: thesis: verum

end;

end;