theorem Th16: :: JORDAN14:16

for C being Simple_closed_curve
for n being Nat st n is_sufficiently_large_for C holds
UBD C c= LeftComp (Span (C,n))