theorem LemmaWA: :: FUZIMPL2:14

for I being BinOp of [.0,1.] st I is satisfying_(NP) holds
( I is satisfying_(I4) & I is satisfying_(I5) )