let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat holds [1,1] in Indices (Gauge (R,n))
let n be Nat; :: thesis: [1,1] in Indices (Gauge (R,n))
A1: len (Gauge (R,n)) = width (Gauge (R,n)) by JORDAN8:def 1;
1 <= len (Gauge (R,n)) by Lm3;
hence [1,1] in Indices (Gauge (R,n)) by A1, MATRIX_0:30; :: thesis: verum