let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for n being 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 Nat st n is_sufficiently_large_for C & P is_outside_component_of C holds
P misses L~ (Span (C,n))
let n be 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
A4: UBD C c= LeftComp (Span (C,n)) by A1, Th16;
consider x being object such that
A5: x in P and
A6: x in L~ (Span (C,n)) by A3, XBOOLE_0:3;
P c= UBD C by A2, JORDAN2C:23;
then x in UBD C by A5;
hence contradiction by A6, A4, GOBRD14:17; :: thesis: verum