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 AS0: ( 0 <= x & 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
X1: ( x < s & s < y ) by AS0, XREAL_1:7;

now

per cases ( 0 = x or 0 < x ) by AS0;

case XK0: 0 = x ; :: thesis: ( 0 < s & x < y / (1 + s) & y / (1 + s) < y )

set s0 = s;
y < y * (1 + s) by X1, AS0, XREAL_1:31, XREAL_1:157;
hence ( 0 < s & x < y / (1 + s) & y / (1 + s) < y ) by X1, XK0, XREAL_1:85, XREAL_1:141; :: thesis: verum

end;

case XK1: 0 < x ; :: thesis: ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y )

set s0 = (s / x) - 1;
RX2: ( 0 < 1 + ((s / x) - 1) & 1 < 1 + ((s / x) - 1) ) by X1, XK1, XREAL_1:189;
(1 + ((s / x) - 1)) * x = (x / x) * s by XCMPLX_1:76;
then (1 + ((s / x) - 1)) * x = 1 * s by XK1, XCMPLX_1:60;
then RX3: (((1 + ((s / x) - 1)) " ) * (1 + ((s / x) - 1))) * x = s * ((1 + ((s / x) - 1)) " ) ;
LV1: (1 + ((s / x) - 1)) " = 1 / (1 + ((s / x) - 1)) by XCMPLX_1:217;
LV3: ((1 + ((s / x) - 1)) " ) * (1 + ((s / x) - 1)) = 1 by LV1, RX2, XCMPLX_1:107;
LV5: s * ((1 + ((s / x) - 1)) " ) = (s * 1) / (1 + ((s / x) - 1)) by LV1, XCMPLX_1:75;
y < y * (1 + ((s / x) - 1)) by AS0, RX2, XREAL_1:157;
hence ( 0 < (s / x) - 1 & x < y / (1 + ((s / x) - 1)) & y / (1 + ((s / x) - 1)) < y ) by RX2, X1, RX3, LV3, LV5, 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