let x1, y1, x2, y2 be object ; :: thesis: for X being set st x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]} holds
( x1 = x2 & y1 = y2 )
let X be set ; :: thesis: ( x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]} implies ( x1 = x2 & y1 = y2 ) )
assume that
A1: x1 in X and
A2: x2 in X ; :: thesis: ( not {x1,[y1,X]} = {x2,[y2,X]} or ( x1 = x2 & y1 = y2 ) )
assume A3: {x1,[y1,X]} = {x2,[y2,X]} ; :: thesis: ( x1 = x2 & y1 = y2 )

per cases ( ( x1 = x2 & [y1,X] = [y2,X] ) or ( x1 = x2 & [y1,X] = x2 ) or ( x1 = [y2,X] & [y1,X] = x2 ) or ( x1 = [y2,X] & [y1,X] = [y2,X] ) ) by A3, ZFMISC_1:6;

suppose ( x1 = x2 & [y1,X] = [y2,X] ) ; :: thesis: ( x1 = x2 & y1 = y2 )

hence ( x1 = x2 & y1 = y2 ) by XTUPLE_0:1; :: thesis: verum

end;

suppose ( x1 = x2 & [y1,X] = x2 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

hence ( x1 = x2 & y1 = y2 ) by Th1, A2; :: thesis: verum

end;

suppose ( x1 = [y2,X] & [y1,X] = x2 ) ; :: thesis: ( x1 = x2 & y1 = y2 )

hence ( x1 = x2 & y1 = y2 ) by Th1, A2; :: thesis: verum

end;

suppose ( x1 = [y2,X] & [y1,X] = [y2,X] ) ; :: thesis: ( x1 = x2 & y1 = y2 )

hence ( x1 = x2 & y1 = y2 ) by Th1, A1; :: thesis: verum

end;

end;