let x, y be object ; :: thesis: ( {x} \ {y} = {} implies x = y )
assume {x} \ {y} = {} ; :: thesis: x = y
then x in {y} by Lm1, XBOOLE_1:37;
hence x = y by TARSKI:def 1; :: thesis: verum