theorem Prop136a: :: FUZIMPL3:12

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