theorem QuoIn01: :: FUZIMPL1:6

for a, b being Element of [.0,1.] st a > b holds
b / a in [.0,1.]