let X be without_pairs set ; :: thesis: for Y being Relation holds X \ Y = X
let Y be Relation; :: thesis: X \ Y = X

now

given x being set such that A1: x in X /\ Y ; :: thesis: contradiction
( x in X & x in Y ) by A1, XBOOLE_0:def 4;
then ex a, b being set st x = [a,b] by RELAT_1:def 1;
hence contradiction by A1, FACIRC_1:def 2; :: thesis: verum

end;

then X /\ Y = {} by XBOOLE_0:7;
then X misses Y by XBOOLE_0:def 7;
hence X \ Y = X by XBOOLE_1:83; :: thesis: verum