let C be Simple_closed_curve; :: thesis: for n being Nat st n is_sufficiently_large_for C holds
UBD C misses L~ (Span (C,n))
let n be Nat; :: thesis: ( n is_sufficiently_large_for C implies UBD C misses L~ (Span (C,n)) )
assume A1: n is_sufficiently_large_for C ; :: thesis: UBD C misses L~ (Span (C,n))
assume UBD C meets L~ (Span (C,n)) ; :: thesis: 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; :: thesis: verum