let x, y1, y2 be object ; :: thesis: ( {x} = {y1,y2} implies x = y1 )
assume {x} = {y1,y2} ; :: thesis: x = y1
then y1 in {x} by TARSKI:def 2;
hence x = y1 by TARSKI:def 1; :: thesis: verum