let x1, x2, y1, y2 be set ; :: thesis: ( len (x1,x2 ][ y1,y2) = 2 & width (x1,x2 ][ y1,y2) = 2 & Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] )
set M = x1,x2 ][ y1,y2;
thus A1: len (x1,x2 ][ y1,y2) = 2 by FINSEQ_1:61; :: thesis: ( width (x1,x2 ][ y1,y2) = 2 & Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] )
rng (x1,x2 ][ y1,y2) = {<*x1,x2*>,<*y1,y2*>} by FINSEQ_2:147;
then A2: <*x1,x2*> in rng (x1,x2 ][ y1,y2) by TARSKI:def 2;
len <*x1,x2*> = 2 by FINSEQ_1:61;
hence width (x1,x2 ][ y1,y2) = 2 by A1, A2, MATRIX_1:def 4; :: thesis: Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):]
hence Indices (x1,x2 ][ y1,y2) = [:(Seg 2),(Seg 2):] by A1, FINSEQ_1:def 3; :: thesis: verum