let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span C,n)
let P be Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span C,n)
let n be Element of NAT ; :: thesis: ( n is_sufficiently_large_for C & P is_outside_component_of C implies P misses L~ (Span C,n) )
assume that
A1: n is_sufficiently_large_for C and
A2: P is_outside_component_of C and
A3: P meets L~ (Span C,n) ; :: thesis: contradiction
consider x being set such that
A4: ( x in P & x in L~ (Span C,n) ) by A3, XBOOLE_0:3;
P c= UBD C by A2, JORDAN2C:27;
then A5: x in UBD C by A4;
UBD C c= LeftComp (Span C,n) by A1, Th17;
hence contradiction by A4, A5, GOBRD14:27; :: thesis: verum