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