let n be Element of 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:102;
then (2 |^ (n -' 1)) + 2 > 0 + 2 by XREAL_1:8;
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:107;
hence X-SpanStart (C,n) < len (Gauge (C,n)) by XREAL_1:10; :: thesis: verum