let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st q in UBD C & p in BDD C holds
dist (q,C) < dist (q,p)
let p, q be Point of (TOP-REAL 2); :: thesis: ( q in UBD C & p in BDD C implies dist (q,C) < dist (q,p) )
assume that
A1: q in UBD C and
A2: p in BDD C and
A3: dist (q,C) >= dist (q,p) ; :: thesis: contradiction
A4: UBD C is_a_component_of C ` by JORDAN2C:124;

now :: thesis: not LSeg (p,q) meets C

assume LSeg (p,q) meets C ; :: thesis: contradiction
then consider x being object such that
A5: x in LSeg (p,q) and
A6: x in C by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A7: dist (q,C) <= dist (q,x) by A6, JORDAN1K:50;
C misses BDD C by JORDAN1A:7;
then x <> p by A2, A6, XBOOLE_0:3;
hence contradiction by A3, A5, A7, JORDAN1K:30, XXREAL_0:2; :: thesis: verum

end;

then A8: LSeg (p,q) c= C ` by SUBSET_1:23;
q in LSeg (p,q) by RLTOPSP1:68;
then A9: LSeg (p,q) meets UBD C by A1, XBOOLE_0:3;
A10: BDD C = union { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by JORDAN2C:def 4;
then consider X being set such that
A11: p in X and
A12: X in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by A2, TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A13: X = B and
A14: B is_inside_component_of C by A12;
B c= BDD C by A10, A12, A13, ZFMISC_1:74;
then A15: B misses UBD C by JORDAN2C:24, XBOOLE_1:63;
p in LSeg (p,q) by RLTOPSP1:68;
then A16: LSeg (p,q) meets B by A11, A13, XBOOLE_0:3;
B is_a_component_of C ` by A14, JORDAN2C:def 2;
then UBD C = B by A8, A4, A9, A16, JORDAN9:1;
hence contradiction by A15; :: thesis: verum