let x, y1, y2 be set ; :: thesis: ( {x} = {y1,y2} implies y1 = y2 )
assume {x} = {y1,y2} ; :: thesis: y1 = y2
then ( x = y1 & x = y2 ) by Th8;
hence y1 = y2 ; :: thesis: verum