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) )
2 < X-SpanStart C,n by Th58;
then A1: ((X-SpanStart C,n) -' 1) + 1 = X-SpanStart C,n by XREAL_1:237, XXREAL_0:2;
1 < X-SpanStart C,n by Th58, XXREAL_0:2;
hence 1 <= (X-SpanStart C,n) -' 1 by A1, NAT_1:13; :: thesis: (X-SpanStart C,n) -' 1 < len (Gauge C,n)
( X-SpanStart C,n < len (Gauge C,n) & (X-SpanStart C,n) -' 1 <= X-SpanStart C,n ) by Th58, NAT_D:44;
hence (X-SpanStart C,n) -' 1 < len (Gauge C,n) by XXREAL_0:2; :: thesis: verum