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) )
A1: 2 in Seg 2 by FINSEQ_1:4, TARSKI:def 2;
( Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] & 1 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 A1, ZFMISC_1:106; :: thesis: verum