theorem Th1: :: LOPBAN_6:1

for x, y being Real st 0 <= x & x < y holds
ex s0 being Real st
( 0 < s0 & x < y / (1 + s0) & y / (1 + s0) < y )