theorem :: FUZIMPL4:9

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation holds
( I is N -satisfying_CP iff I is N -satisfying_L-CP ) by Lemma15312, Lemma15323, Lemma15331;