let C be being_simple_closed_curve Subset of (TOP-REAL 2); 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); ( 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)
; contradiction
A4:
UBD C is_a_component_of C `
by JORDAN2C:124;
now not LSeg (p,q) meets Cassume
LSeg (
p,
q)
meets C
;
contradictionthen 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;
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; verum