let x, y, x1, y1 be set ; :: thesis: ( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) )
( x = x1 & y = y1 iff ( x in {x1} & y in {y1} ) ) by TARSKI:def 1;
hence ( [x,y] in [:{x1},{y1}:] iff ( x = x1 & y = y1 ) ) by Lm17; :: thesis: verum