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