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;
A2: 4 <= len (Gauge R,n) by JORDAN8:13;
then A3: 2 <= len (Gauge R,n) by XXREAL_0:2;
1 <= len (Gauge R,n) by A2, XXREAL_0:2;
hence [1,2] in Indices (Gauge R,n) by A1, A3, MATRIX_1:37; :: thesis: verum