let x, X, y be set ; :: thesis: ( x in X & ( not y in X or x = y ) implies {x,y} /\ X = {x} )
assume A1: ( x in X & ( 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 iff ( z in {x,y} & z in X ) ) by XBOOLE_0:def 4;
hence ( z in {x,y} /\ X iff z = x ) by A1, TARSKI:def 2; :: thesis: verum

end;

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