for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for n being Nat st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span (C,n))