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_of (TOP-REAL 2) | (C ` ) & VP is bounded Subset of (Euclid 2) ) by A2, JORDAN2C:17;
UMP C in LSeg |[0 ,3]|,(UMP C) by RLTOPSP1:69;
then {(UMP C)} c= LSeg |[0 ,3]|,(UMP C) by ZFMISC_1:37;
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, XBOOLE_1:1;
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:43;
hence LSeg |[0 ,3]|,(UMP C) misses P by A4, A6, XBOOLE_1:70; :: thesis: verum