let x, y be object ; :: thesis: for X being set holds
( not {x,y} /\ X = {x} or not y in X or x = y )
let X be set ; :: thesis: ( not {x,y} /\ X = {x} or not y in X or x = y )
A1: y in {x,y} by TARSKI:def 2;
assume ( {x,y} /\ X = {x} & y in X ) ; :: thesis: x = y
then y in {x} by A1, XBOOLE_0:def 4;
hence x = y by TARSKI:def 1; :: thesis: verum