theorem Th34: :: JORDAN14:34

for C being Simple_closed_curve
for n, m being Nat st n is_sufficiently_large_for C & n <= m holds
L~ (Span (C,m)) c= Cl (LeftComp (Span (C,n)))