theorem Rosnie: :: FUZIMPL3:6

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