let x, y be object ; :: thesis: for x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )
let x1, y1 be set ; :: 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