theorem :: FUZIMPL4:10
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_R-CP ) by Lemma15312, Lemma15323, Lemma15331;