theorem :: FUZIMPL3:17

for f being bijective decreasing UnOp of [.0,1.] holds
( f . 0 = 1 & f . 1 = 0 )