let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C misses RightComp (Span C,n)
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies C misses RightComp (Span C,n) )
assume A1: n is_sufficiently_large_for C ; :: thesis: C misses RightComp (Span C,n)
set f = Span C,n;
A2: C misses L~ (Span C,n) by A1, Th9;
A3: C meets LeftComp (Span C,n) by A1, Th10;
assume A4: C meets RightComp (Span C,n) ; :: thesis: contradiction
RightComp (Span C,n) is_a_component_of (L~ (Span C,n)) ` by GOBOARD9:def 2;
then consider L being Subset of ((TOP-REAL 2) | ((L~ (Span C,n)) ` )) such that
A5: L = RightComp (Span C,n) and
A6: L is_a_component_of (TOP-REAL 2) | ((L~ (Span C,n)) ` ) by CONNSP_1:def 6;
LeftComp (Span C,n) is_a_component_of (L~ (Span C,n)) ` by GOBOARD9:def 1;
then consider R being Subset of ((TOP-REAL 2) | ((L~ (Span C,n)) ` )) such that
A7: R = LeftComp (Span C,n) and
A8: R is_a_component_of (TOP-REAL 2) | ((L~ (Span C,n)) ` ) by CONNSP_1:def 6;
C c= the carrier of ((TOP-REAL 2) | ((L~ (Span C,n)) ` ))

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in the carrier of ((TOP-REAL 2) | ((L~ (Span C,n)) ` )) )
assume c in C ; :: thesis: c in the carrier of ((TOP-REAL 2) | ((L~ (Span C,n)) ` ))
then ( c in the carrier of (TOP-REAL 2) & not c in L~ (Span C,n) ) by A2, XBOOLE_0:3;
then c in (L~ (Span C,n)) ` by SUBSET_1:50;
hence c in the carrier of ((TOP-REAL 2) | ((L~ (Span C,n)) ` )) by PRE_TOPC:29; :: thesis: verum

end;

then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Span C,n)) ` )) ;
C1 is connected by CONNSP_1:24;
hence contradiction by A3, A4, A5, A6, A7, A8, JORDAN2C:100, SPRECT_4:7; :: thesis: verum