let x1,

y1,

x2,

y2,

x3,

y3 be

set ;

( [[x1,x2],x3] = [[y1,y2],y3] implies ( x1 = y1 & x2 = y2 ) )
assume
[[x1,x2],x3] = [[y1,y2],y3]
;

( x1 = y1 & x2 = y2 )
then
[x1,x2] = [y1,y2]
by XTUPLE_0:1;

hence
( x1 = y1 &

x2 = y2 )

by XTUPLE_0:1;

verum