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:10;
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:36; :: thesis: verum