let x1, x2, y, y1, y2, x be set ; :: thesis: ( [[x1,x2],y] `11 = x1 & [[x1,x2],y] `12 = x2 & [x,[y1,y2]] `21 = y1 & [x,[y1,y2]] `22 = y2 )
( [[x1,x2],y] `1 = [x1,x2] & [x,[y1,y2]] `2 = [y1,y2] ) by Def1, Def2;
hence ( [[x1,x2],y] `11 = x1 & [[x1,x2],y] `12 = x2 & [x,[y1,y2]] `21 = y1 & [x,[y1,y2]] `22 = y2 ) by Def1, Def2; :: thesis: verum