theorem :: FUZIMPL4:24
for I being satisfying_(NP) satisfying_(EP) Fuzzy_Implication holds
( FNegation I is negation-strong iff I is FNegation I -satisfying_CP ) by Lemma154va, Lemma156ii;