theorem NonInc: :: FUZIMPL3:7

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