theorem LemmaZA: :: FUZIMPL2:15

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