let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C c= LeftComp (Span (C,n))
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C implies C c= LeftComp (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; :: thesis: C c= LeftComp (Span (C,n))
let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in LeftComp (Span (C,n)) )
set f = Span (C,n);
assume A2: c in C ; :: thesis: c in LeftComp (Span (C,n))
C misses L~ (Span (C,n)) by A1, Th9;
then A3: not c in L~ (Span (C,n)) by A2, XBOOLE_0:3;
C misses RightComp (Span (C,n)) by A1, Th11;
then not c in RightComp (Span (C,n)) by A2, XBOOLE_0:3;
hence c in LeftComp (Span (C,n)) by A2, A3, GOBRD14:28; :: thesis: verum