theorem :: BKMODEL3:1

for x, y being Real st x * y < 0 holds
( 0 < x / (x - y) & x / (x - y) < 1 )