let n be Nat; 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); ( 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)
; 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; verum