theorem Th1: :: SIN_COS6:1

for r, s being Real st 0 <= r & r < s holds
[\(r / s)/] = 0