let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds [1,2] in Indices (Gauge R,n)
let n be Element of NAT ; :: thesis: [1,2] in Indices (Gauge R,n)
A1: len (Gauge R,n) = width (Gauge R,n) by JORDAN8:def 1;
4 <= len (Gauge R,n) by JORDAN8:13;
then ( 1 <= len (Gauge R,n) & 2 <= len (Gauge R,n) ) by XXREAL_0:2;
hence [1,2] in Indices (Gauge R,n) by A1, MATRIX_1:37; :: thesis: verum