theorem Th50: :: JORDAN1H:50

for n being Nat
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)) )