let T be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat holds len (Gauge T,n) >= 4
let n be Nat; :: thesis: len (Gauge T,n) >= 4
set G = Gauge T,n;
A1: len (Gauge T,n) = (2 |^ n) + 3 by Def1;
2 |^ n >= n + 1 by NEWTON:104;
then len (Gauge T,n) >= (n + 1) + 3 by A1, XREAL_1:8;
then ( len (Gauge T,n) >= n + (3 + 1) & n + 4 >= 4 ) by NAT_1:12;
hence len (Gauge T,n) >= 4 by XXREAL_0:2; :: thesis: verum