let x, y be Real; :: thesis: ( 0 <= x & x < y implies ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) )

assume that
A1: 0 <= x and
A2: x < y ; :: thesis: ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )

ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
proof
consider s being Real such that
A3: x < s and
A4: s < y by ;
now :: thesis: ( ( 0 = x & 0 < s & x < y / (1 + s) & y / (1 + s) < y ) or ( 0 < x & 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) )
per cases ( 0 = x or 0 < x ) by A1;
case A5: 0 = x ; :: thesis: ( 0 < s & x < y / (1 + s) & y / (1 + s) < y )
set s0 = s;
y < y * (1 + s) by ;
hence ( 0 < s & x < y / (1 + s) & y / (1 + s) < y ) by ; :: thesis: verum
end;
case A6: 0 < x ; :: thesis: ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y )
set s0 = (s / x) - 1;
A7: (1 + ((s / x) - 1)) " = 1 / (1 + ((s / x) - 1)) by XCMPLX_1:215;
then A8: s * ((1 + ((s / x) - 1)) ") = (s * 1) / (1 + ((s / x) - 1)) by XCMPLX_1:74;
(1 + ((s / x) - 1)) * x = (x / x) * s by XCMPLX_1:75;
then (1 + ((s / x) - 1)) * x = 1 * s by ;
then A9: (((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1))) * x = s * ((1 + ((s / x) - 1)) ") ;
0 < 1 + ((s / x) - 1) by ;
then A10: ((1 + ((s / x) - 1)) ") * (1 + ((s / x) - 1)) = 1 by ;
A11: 1 < 1 + ((s / x) - 1) by ;
then y < y * (1 + ((s / x) - 1)) by ;
hence ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) by ; :: thesis: verum
end;
end;
end;
hence ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum
end;
hence ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum