let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
C misses L~ (Span C,n)
let n be Element of 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 f = Span C,n;
set G = Gauge C,n;
assume not C misses L~ (Span C,n) ; :: thesis: contradiction
then consider c being set such that
A2: ( c in C & c in L~ (Span C,n) ) by XBOOLE_0:3;
L~ (Span C,n) = union { (LSeg (Span C,n),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span C,n) ) } by TOPREAL1:def 6;
then consider Z being set such that
A3: c in Z and
A4: Z in { (LSeg (Span C,n),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (Span C,n) ) } by A2, TARSKI:def 4;
consider i being Element of NAT such that
A5: Z = LSeg (Span C,n),i and
A6: ( 1 <= i & i + 1 <= len (Span C,n) ) by A4;
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 A6, GOBRD13:30;
then A7: c in right_cell (Span C,n),i,(Gauge C,n) by A3, A5, XBOOLE_0:def 4;
right_cell (Span C,n),i,(Gauge C,n) misses C by A1, A6, Th8;
hence contradiction by A2, A7, XBOOLE_0:3; :: thesis: verum