let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C holds
LSeg ((LMP C),|[0,(- 3)]|) misses P
let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies LSeg ((LMP C),|[0,(- 3)]|) misses P )
set m = LMP C;
set L = LSeg ((LMP C),|[0,(- 3)]|);
assume that
A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C and
A2: P is_inside_component_of C ; :: thesis: LSeg ((LMP C),|[0,(- 3)]|) misses P
A3: ex VP being Subset of ((TOP-REAL 2) | (C `)) st
( VP = P & VP is a_component & VP is bounded Subset of (Euclid 2) ) by A2, JORDAN2C:13;
LMP C in LSeg ((LMP C),|[0,(- 3)]|) by RLTOPSP1:68;
then {(LMP C)} c= LSeg ((LMP C),|[0,(- 3)]|) by ZFMISC_1:31;
then A4: LSeg ((LMP C),|[0,(- 3)]|) = ((LSeg ((LMP C),|[0,(- 3)]|)) \ {(LMP C)}) \/ {(LMP C)} by XBOOLE_1:45;
A5: (LSeg ((LMP C),|[0,(- 3)]|)) \ {(LMP C)} c= (south_halfline (LMP C)) \ {(LMP C)} by A1, Th88, XBOOLE_1:33;
(south_halfline (LMP C)) \ {(LMP C)} c= UBD C by Th13;
then (LSeg ((LMP C),|[0,(- 3)]|)) \ {(LMP C)} c= UBD C by A5;
then A6: (LSeg ((LMP C),|[0,(- 3)]|)) \ {(LMP C)} misses P by A2, Th14, XBOOLE_1:63;
{(LMP C)} misses P by A3, Lm4, JORDAN21:31;
hence LSeg ((LMP C),|[0,(- 3)]|) misses P by A4, A6, XBOOLE_1:70; :: thesis: verum