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)
A1: len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
n -' 1 <= n by NAT_D:44;
then 2 |^ (n -' 1) <= 2 |^ n by PREPOWER:107;
hence X-SpanStart C,n < len (Gauge C,n) by A1, XREAL_1:10; :: thesis: verum