let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat holds [2,1] in Indices (Gauge (R,n))
let n be Nat; :: thesis: [2,1] 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 [2,1] in Indices (Gauge (R,n)) by A1, A3, MATRIX_0:30; :: thesis: verum