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