theorem :: FUZIMPL3:11

for I being Fuzzy_Implication
for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) is Fuzzy_Implication ;