let x, y be real number ; :: thesis: ( 0 <= x & x < y implies ex s0 being real number 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 number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )
ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )

proof

consider s being real number such that
A3: x < s and
A4: s < y by A2, XREAL_1:7;

now

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 A1, A3, A4, XREAL_1:31, XREAL_1:157;
hence ( 0 < s & x < y / (1 + s) & y / (1 + s) < y ) by A3, A4, A5, XREAL_1:85, XREAL_1:141; :: 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:217;
then A8: s * ((1 + ((s / x) - 1)) " ) = (s * 1) / (1 + ((s / x) - 1)) by XCMPLX_1:75;
(1 + ((s / x) - 1)) * x = (x / x) * s by XCMPLX_1:76;
then (1 + ((s / x) - 1)) * x = 1 * s by A6, XCMPLX_1:60;
then A9: (((1 + ((s / x) - 1)) " ) * (1 + ((s / x) - 1))) * x = s * ((1 + ((s / x) - 1)) " ) ;
0 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:189;
then A10: ((1 + ((s / x) - 1)) " ) * (1 + ((s / x) - 1)) = 1 by A7, XCMPLX_1:107;
A11: 1 < 1 + ((s / x) - 1) by A3, A6, XREAL_1:189;
then y < y * (1 + ((s / x) - 1)) by A1, A2, XREAL_1:157;
hence ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) by A4, A11, A9, A10, A8, XREAL_1:52, XREAL_1:76, XREAL_1:85; :: thesis: verum

end;

end;

end;

hence ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum

end;

hence ex s0 being real number st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y ) ; :: thesis: verum