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