theorem Decreas: :: FUZIMPL3:8

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