theorem Th13: :: JORDAN14:13

for C being Simple_closed_curve
for n being Nat st n is_sufficiently_large_for C holds
BDD (L~ (Span (C,n))) c= BDD C