theorem Th6: :: JORDAN14:6

for C being Simple_closed_curve
for n being Nat st n is_sufficiently_large_for C holds
SpanStart (C,n) in BDD C