theorem :: FUZIMPL4:5

for I being BinOp of [.0,1.]
for N being negation-strict Fuzzy_Negation
for N1 being Fuzzy_Negation st N ~ = N1 holds
( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP )