let C be Simple_closed_curve; :: thesis: for n being Element of NAT st n is_sufficiently_large_for C holds
UBD C misses L~ (Span C,n)
let n be Element of 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)
A2: UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def 6;
assume UBD C meets L~ (Span C,n) ; :: thesis: contradiction
then consider x being set such that
A3: ( x in UBD C & x in L~ (Span C,n) ) by XBOOLE_0:3;
consider Z being set such that
A4: ( x in Z & Z in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } ) by A2, A3, TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A5: ( Z = B & B is_outside_component_of C ) by A4;
B misses L~ (Span C,n) by A1, A5, Th20;
hence contradiction by A3, A4, A5, XBOOLE_0:3; :: thesis: verum