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

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