let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds [1,1] in Indices (Gauge (R,n))
let n be Element of 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_1:36; :: thesis: verum