let x, x1, y, y1 be object ; :: thesis: ( [x,y] in {[x1,y1]} implies ( x = x1 & y = y1 ) )
assume [x,y] in {[x1,y1]} ; :: thesis: ( x = x1 & y = y1 )
then [x,y] = [x1,y1] by TARSKI:def 1;
hence ( x = x1 & y = y1 ) by XTUPLE_0:1; :: thesis: verum