:: deftheorem BIDef defines ConjImpl FUZIMPL3:def 2 :
for f being BinOp of [.0,1.]
for h being bijective increasing UnOp of [.0,1.]
for b₃ being BinOp of [.0,1.] holds
( b₃ = ConjImpl (f,h) iff for x1, x2 being Element of [.0,1.] holds b₃ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) );