let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C meets LeftComp (Span C,n)
let n be Element of 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)
A2: 1 + 1 <= len (Span C,n) by GOBOARD7:36, XXREAL_0:2;
then left_cell (Span C,n),1,(Gauge C,n) meets C by A1, Th8;
then A3: (left_cell (Span C,n),1,(Gauge C,n)) \ (L~ (Span C,n)) meets C by A1, Th9, XBOOLE_1:84;
Span C,n is_sequence_on Gauge C,n by A1, JORDAN13:def 1;
then (left_cell (Span C,n),1,(Gauge C,n)) \ (L~ (Span C,n)) c= LeftComp (Span C,n) by A2, JORDAN9:29;
hence C meets LeftComp (Span C,n) by A3, XBOOLE_1:63; :: thesis: verum