:: deftheorem CNDef defines ConjNeg FUZIMPL3:def 22 :
for f being UnOp of [.0,1.]
for h being bijective increasing UnOp of [.0,1.]
for b₃ being UnOp of [.0,1.] holds
( b₃ = ConjNeg (f,h) iff for x being Element of [.0,1.] holds b₃ . x = (h ") . (f . (h . x)) );