let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
C misses RightComp (Span (C,n))
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies C misses RightComp (Span (C,n)) )
set f = Span (C,n);
RightComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def 2;
then A1: ex L being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st
( L = RightComp (Span (C,n)) & L is a_component ) by CONNSP_1:def 6;
LeftComp (Span (C,n)) is_a_component_of (L~ (Span (C,n))) ` by GOBOARD9:def 1;
then A2: ex R being Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) st
( R = LeftComp (Span (C,n)) & R is a_component ) by CONNSP_1:def 6;
assume A3: n is_sufficiently_large_for C ; :: thesis: C misses RightComp (Span (C,n))
then A4: C misses L~ (Span (C,n)) by Th8;
C c= the carrier of ((TOP-REAL 2) | ((L~ (Span (C,n))) `))

proof

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

end;

then reconsider C1 = C as Subset of ((TOP-REAL 2) | ((L~ (Span (C,n))) `)) ;
assume A6: C meets RightComp (Span (C,n)) ; :: thesis: contradiction
A7: C1 is connected by CONNSP_1:23;
C meets LeftComp (Span (C,n)) by A3, Th9;
hence contradiction by A6, A1, A2, A7, JORDAN2C:92, SPRECT_4:6; :: thesis: verum