:: deftheorem defines satisfying_L-CP FUZIMPL4:def 7 :
for I being Fuzzy_Implication holds
( I is satisfying_L-CP iff I is FNegation I -satisfying_L-CP );