let x1, y1, x2, y2, X be set ; :: thesis: ( x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]} implies ( x1 = x2 & y1 = y2 ) )
assume that
Ax1: x1 in X and
Ax2: x2 in X ; :: thesis: ( not {x1,[y1,X]} = {x2,[y2,X]} or ( x1 = x2 & y1 = y2 ) )
assume A: {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 A, 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 Aux1, Ax2; :: thesis: verum

end;

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

hence ( x1 = x2 & y1 = y2 ) by Aux1, Ax2; :: thesis: verum

end;

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

hence ( x1 = x2 & y1 = y2 ) by Aux1, Ax1; :: thesis: verum

end;

end;