:: deftheorem defines satisfying_CP FUZIMPL4:def 6 :
for I being Fuzzy_Implication holds
( I is satisfying_CP iff I is FNegation I -satisfying_CP );