theorem Lemma154vb: :: FUZIMPL4:16
for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) )