let n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 1 <= (X-SpanStart C,n) -' 1 & (X-SpanStart C,n) -' 1 < len (Gauge C,n) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= (X-SpanStart C,n) -' 1 & (X-SpanStart C,n) -' 1 < len (Gauge C,n) )
A1: 2 < X-SpanStart C,n by Th58;
then A2: 1 < X-SpanStart C,n by XXREAL_0:2;
((X-SpanStart C,n) -' 1) + 1 = X-SpanStart C,n by A1, XREAL_1:237, XXREAL_0:2;
hence 1 <= (X-SpanStart C,n) -' 1 by A2, NAT_1:13; :: thesis: (X-SpanStart C,n) -' 1 < len (Gauge C,n)
A3: X-SpanStart C,n < len (Gauge C,n) by Th58;
(X-SpanStart C,n) -' 1 <= X-SpanStart C,n by NAT_D:44;
hence (X-SpanStart C,n) -' 1 < len (Gauge C,n) by A3, XXREAL_0:2; :: thesis: verum