:: deftheorem defines is_sufficiently_large_for JORDAN1H:def 3 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( n is_sufficiently_large_for C iff ex j being Nat st
( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) );