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 Lx4;
hence y1 = y2 by A1, Lx4; :: thesis: verum