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