let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
C meets LeftComp (Span (C,n))
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies C meets LeftComp (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; :: thesis: C meets LeftComp (Span (C,n))
then A2: Span (C,n) is_sequence_on Gauge (C,n) by JORDAN13:def 1;
A3: 1 + 1 <= len (Span (C,n)) by GOBOARD7:34, XXREAL_0:2;
then left_cell ((Span (C,n)),1,(Gauge (C,n))) meets C by A1, Th7;
then (left_cell ((Span (C,n)),1,(Gauge (C,n)))) \ (L~ (Span (C,n))) meets C by A1, Th8, XBOOLE_1:84;
hence C meets LeftComp (Span (C,n)) by A3, A2, JORDAN9:27, XBOOLE_1:63; :: thesis: verum