let C be Simple_closed_curve; for n being Nat st n is_sufficiently_large_for C holds
C misses L~ (Span (C,n))
let n be Nat; ( n is_sufficiently_large_for C implies C misses L~ (Span (C,n)) )
assume A1:
n is_sufficiently_large_for C
; C misses L~ (Span (C,n))
set G = Gauge (C,n);
set f = Span (C,n);
assume
not C misses L~ (Span (C,n))
; 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; verum