let X be without_pairs set ; :: thesis: for Y being Relation holds X \ Y = X
let Y be Relation; :: thesis: X \ Y = X
X /\ Y = {} ;
then X misses Y by XBOOLE_0:def 7;
hence X \ Y = X by XBOOLE_1:83; :: thesis: verum