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 (|[0,3]|,(UMP C)) 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 (|[0,3]|,(UMP C)) misses P )
set m = UMP C;
set L = LSeg (|[0,3]|,(UMP C));
assume that
A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C and
A2: P is_inside_component_of C ; :: thesis: LSeg (|[0,3]|,(UMP C)) 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;
UMP C in LSeg (|[0,3]|,(UMP C)) by RLTOPSP1:68;
then {(UMP C)} c= LSeg (|[0,3]|,(UMP C)) by ZFMISC_1:31;
then A4: LSeg (|[0,3]|,(UMP C)) = ((LSeg (|[0,3]|,(UMP C))) \ {(UMP C)}) \/ {(UMP C)} by XBOOLE_1:45;
A5: (LSeg (|[0,3]|,(UMP C))) \ {(UMP C)} c= (north_halfline (UMP C)) \ {(UMP C)} by A1, Th87, XBOOLE_1:33;
(north_halfline (UMP C)) \ {(UMP C)} c= UBD C by Th12;
then (LSeg (|[0,3]|,(UMP C))) \ {(UMP C)} c= UBD C by A5;
then A6: (LSeg (|[0,3]|,(UMP C))) \ {(UMP C)} misses P by A2, Th14, XBOOLE_1:63;
{(UMP C)} misses P by A3, Lm4, JORDAN21:30;
hence LSeg (|[0,3]|,(UMP C)) misses P by A4, A6, XBOOLE_1:70; :: thesis: verum