Fixed def of not-member-add2-preserves-leq-converse