let x, x1, y, y1 be object ; :: 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 Lm16; :: thesis: verum