let x1, x2, y1, y2 be object ; :: 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:44; :: 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:127;
then A2: <*x1,x2*> in rng ((x1,x2) ][ (y1,y2)) by TARSKI:def 2;
len <*x1,x2*> = 2 by FINSEQ_1:44;
hence width ((x1,x2) ][ (y1,y2)) = 2 by A1, A2, Def3; :: 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