let x1, y1, x2, y2, x3, y3 be set ; :: thesis: ( [[x1,x2],x3] = [[y1,y2],y3] implies ( x1 = y1 & x2 = y2 ) )
assume [[x1,x2],x3] = [[y1,y2],y3] ; :: thesis: ( x1 = y1 & x2 = y2 )
then [x1,x2] = [y1,y2] by XTUPLE_0:1;
hence ( x1 = y1 & x2 = y2 ) by XTUPLE_0:1; :: thesis: verum