:: deftheorem defines -satisfying_R-CP FUZIMPL4:def 3 :
for N being Fuzzy_Negation
for I being BinOp of [.0,1.] holds
( I is N -satisfying_R-CP iff for x, y being Element of [.0,1.] holds I . (x,(N . y)) = I . (y,(N . x)) );