theorem Prop136d: :: FUZIMPL3:15

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