let n be Element of 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:13;
then 4 - 1 <= (len (Gauge C,n)) - 1 by XREAL_1:15;
hence 3 <= (len (Gauge C,n)) -' 1 by XREAL_0:def 2; :: thesis: verum