theorem Lemma156ii: :: FUZIMPL4:19

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st N = FNegation I & I is satisfying_(EP) holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP )