theorem LemmaAB: :: FUZIMPL2:17

for I being BinOp of [.0,1.] st I is satisfying_(EP) & I is satisfying_(OP) holds
( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) )