let x, y be object ; :: thesis: {x} \ {x,y} = {}
x in {x,y} by TARSKI:def 2;
hence {x} \ {x,y} = {} by Lm1, XBOOLE_1:37; :: thesis: verum