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