let x, z be ExtReal; :: thesis: ( 0 <= x & x < z implies ex y being Real st
( 0 < y & x + y < z ) )
assume that
A1: 0 <= x and
A2: x < z ; :: thesis: ex y being Real st
( 0 < y & x + y < z )
per cases ( 0 < x or 0 = x ) by A1;
suppose A3: 0 < x ; :: thesis: ex y being Real st
( 0 < y & x + y < z )
then 0 < z - x by A2, Th46;
then consider y being Real such that
A4: 0 < y and
A5: y < z - x by Th3;
take y ; :: thesis: ( 0 < y & x + y < z )
A6: x + y <= x + (z - x) by A5, Th36;
A7: x in REAL by A2, A3, XXREAL_0:48;
then A8: x + (z - x) = z by Th22;
x + y <> z by A7, A5, Th22;
hence ( 0 < y & x + y < z ) by A4, A6, A8, XXREAL_0:1; :: thesis: verum
end;
suppose A9: 0 = x ; :: thesis: ex y being Real st
( 0 < y & x + y < z )
consider y being Real such that
A10: ( 0 < y & y < z ) by A1, A2, Th3;
take y ; :: thesis: ( 0 < y & x + y < z )
thus ( 0 < y & x + y < z ) by A9, A10, Th4; :: thesis: verum
end;
end;