theorem LemmaVA: :: FUZIMPL2:13

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