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 A2: len (Gauge T,n) >= (n + 1) + 3 by A1, XREAL_1:8;
n + 4 >= 4 by NAT_1:12;
hence len (Gauge T,n) >= 4 by A2, XXREAL_0:2; :: thesis: verum