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