let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )
2 |^ (n -' 1) > 0 by NEWTON:83;
then (2 |^ (n -' 1)) + 2 > 0 + 2 by XREAL_1:6;
hence 2 < X-SpanStart (C,n) ; :: thesis: X-SpanStart (C,n) < len (Gauge (C,n))
n -' 1 <= n by NAT_D:44;
then ( len (Gauge (C,n)) = (2 |^ n) + 3 & 2 |^ (n -' 1) <= 2 |^ n ) by JORDAN8:def 1, PREPOWER:93;
hence X-SpanStart (C,n) < len (Gauge (C,n)) by XREAL_1:8; :: thesis: verum