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