let R be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat holds 1 <= len (Gauge (R,n))
let n be Nat; :: thesis: 1 <= len (Gauge (R,n))
4 <= len (Gauge (R,n)) by JORDAN8:10;
hence 1 <= len (Gauge (R,n)) by XXREAL_0:2; :: thesis: verum