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

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