theorem RosnieI: :: FUZIMPL3:9

for f being UnOp of [.0,1.] holds
( f is increasing iff for a, b being Element of [.0,1.] st a < b holds
f . a < f . b )