theorem :: FUZIMPL3:33

for I being Fuzzy_Negation
for f being bijective increasing UnOp of [.0,1.] holds ConjNeg (I,f) = ((f ") * I) * f