let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds 3 <= (len (Gauge (C,n))) -' 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 3 <= (len (Gauge (C,n))) -' 1
set G = Gauge (C,n);
4 <= len (Gauge (C,n)) by JORDAN8:10;
then 4 - 1 <= (len (Gauge (C,n))) - 1 by XREAL_1:13;
hence 3 <= (len (Gauge (C,n))) -' 1 by XREAL_0:def 2; :: thesis: verum