let x, X, y be set ; :: thesis: ( x in X & ( not y in X or x = y ) implies {x,y} /\ X = {x} )
assume that
A1: x in X and
A2: ( not y in X or x = y ) ; :: thesis: {x,y} /\ X = {x}
for z being set holds
( z in {x,y} /\ X iff z = x )

proof

let z be set ; :: thesis: ( z in {x,y} /\ X iff z = x )
( ( z in {x,y} /\ X implies ( z in {x,y} & z in X ) ) & ( z in {x,y} & z in X implies z in {x,y} /\ X ) & ( not z in {x,y} or z = x or z = y ) & ( ( z = x or z = y ) implies z in {x,y} ) ) by TARSKI:def 2, XBOOLE_0:def 4;
hence ( z in {x,y} /\ X iff z = x ) by A1, A2; :: thesis: verum

end;

hence {x,y} /\ X = {x} by TARSKI:def 1; :: thesis: verum