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