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