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