let C be being_simple_closed_curve Subset of (TOP-REAL 2); for q, p being Point of (TOP-REAL 2) st q in UBD C & p in BDD C holds
dist q,C < dist q,p
let q, p 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:132;
now assume
LSeg p,
q meets C
;
contradictionthen consider x being
set 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:15;
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:43;
q in LSeg p,q
by RLTOPSP1:69;
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 5;
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:92;
then A15:
B misses UBD C
by JORDAN2C:28, XBOOLE_1:63;
p in LSeg p,q
by RLTOPSP1:69;
then A16:
LSeg p,q meets B
by A11, A13, XBOOLE_0:3;
B is_a_component_of C `
by A14, JORDAN2C:def 3;
then
UBD C = B
by A8, A4, A9, A16, JORDAN9:3;
hence
contradiction
by A15, XBOOLE_1:66; verum