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