let x1, x2, y1, y2 be set ; :: thesis: ( [1,1] in Indices (x1,x2 ][ y1,y2) & [1,2] in Indices (x1,x2 ][ y1,y2) & [2,1] in Indices (x1,x2 ][ y1,y2) & [2,2] in Indices (x1,x2 ][ y1,y2) )
( Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] & 1 in Seg 2 & 2 in Seg 2 ) by Th3, FINSEQ_1:4, TARSKI:def 2;
hence ( [1,1] in Indices (x1,x2 ][ y1,y2) & [1,2] in Indices (x1,x2 ][ y1,y2) & [2,1] in Indices (x1,x2 ][ y1,y2) & [2,2] in Indices (x1,x2 ][ y1,y2) ) by ZFMISC_1:106; :: thesis: verum