let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
C misses L~ (Span (C,n))
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies C misses L~ (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; :: thesis: C misses L~ (Span (C,n))
set G = Gauge (C,n);
set f = Span (C,n);
assume not C misses L~ (Span (C,n)) ; :: thesis: contradiction
then consider c being object such that
A2: c in C and
A3: c in L~ (Span (C,n)) by XBOOLE_0:3;
L~ (Span (C,n)) = union { (LSeg ((Span (C,n)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by TOPREAL1:def 4;
then consider Z being set such that
A4: c in Z and
A5: Z in { (LSeg ((Span (C,n)),i)) where i is Nat : ( 1 <= i & i + 1 <= len (Span (C,n)) ) } by A3, TARSKI:def 4;
consider i being Nat such that
A6: Z = LSeg ((Span (C,n)),i) and
A7: 1 <= i and
A8: i + 1 <= len (Span (C,n)) by A5;
Span (C,n) is_sequence_on Gauge (C,n) by A1, JORDAN13:def 1;
then LSeg ((Span (C,n)),i) = (left_cell ((Span (C,n)),i,(Gauge (C,n)))) /\ (right_cell ((Span (C,n)),i,(Gauge (C,n)))) by A7, A8, GOBRD13:29;
then A9: c in right_cell ((Span (C,n)),i,(Gauge (C,n))) by A4, A6, XBOOLE_0:def 4;
right_cell ((Span (C,n)),i,(Gauge (C,n))) misses C by A1, A7, A8, Th7;
hence contradiction by A2, A9, XBOOLE_0:3; :: thesis: verum