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 )
then A2: x is Real by XXREAL_0:48;
0. < z - x by A1, Th19;
then consider y being R_eal such that
A3: ( 0. < y & y < z - x ) by Th23;
take y ; :: thesis: ( 0. < y & x + y < z & y in REAL )
A4: x + y <= x + (z - x) by A2, A3, Th11;
A5: x + (z - x) = z by A2, Th8;
A6: x + y <> z by A2, A3, Th8;
y is Real by A3, XXREAL_0:48;
hence ( 0. < y & x + y < z & y in REAL ) by A3, A4, A5, A6, XXREAL_0:1; :: thesis: verum