let C be Simple_closed_curve; for n being Nat st n is_sufficiently_large_for C holds
UBD C misses L~ (Span (C,n))
let n be Nat; ( n is_sufficiently_large_for C implies UBD C misses L~ (Span (C,n)) )
assume A1:
n is_sufficiently_large_for C
; UBD C misses L~ (Span (C,n))
assume
UBD C meets L~ (Span (C,n))
; contradiction
then consider x being object such that
A2:
x in UBD C
and
A3:
x in L~ (Span (C,n))
by XBOOLE_0:3;
UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C }
by JORDAN2C:def 5;
then consider Z being set such that
A4:
x in Z
and
A5:
Z in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C }
by A2, TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A6:
Z = B
and
A7:
B is_outside_component_of C
by A5;
B misses L~ (Span (C,n))
by A1, A7, Th19;
hence
contradiction
by A3, A4, A6, XBOOLE_0:3; verum