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 ZFMISC_1:33;
hence ( x1 = y1 & x2 = y2 ) by ZFMISC_1:33; :: thesis: verum