let C be Simple_closed_curve; for n being Nat st n is_sufficiently_large_for C holds
C c= LeftComp (Span (C,n))
let n be Nat; ( n is_sufficiently_large_for C implies C c= LeftComp (Span (C,n)) )
assume A1:
n is_sufficiently_large_for C
; C c= LeftComp (Span (C,n))
let c be object ; TARSKI:def 3 ( not c in C or c in LeftComp (Span (C,n)) )
set f = Span (C,n);
assume A2:
c in C
; c in LeftComp (Span (C,n))
C misses L~ (Span (C,n))
by A1, Th8;
then A3:
not c in L~ (Span (C,n))
by A2, XBOOLE_0:3;
C misses RightComp (Span (C,n))
by A1, Th10;
then
not c in RightComp (Span (C,n))
by A2, XBOOLE_0:3;
hence
c in LeftComp (Span (C,n))
by A2, A3, GOBRD14:18; verum