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
consider VP being Subset of ((TOP-REAL 2) | (C ` )) such that
A3: VP = P and
VP is_a_component_of (TOP-REAL 2) | (C ` ) and
VP is bounded Subset of (Euclid 2) by A2, JORDAN2C:17;
LMP C in LSeg (LMP C),|[0 ,(- 3)]| by RLTOPSP1:69;
then {(LMP C)} c= LSeg (LMP C),|[0 ,(- 3)]| by ZFMISC_1:37;
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, XBOOLE_1:1;
then A6: (LSeg (LMP C),|[0 ,(- 3)]|) \ {(LMP C)} misses P by A2, Th14, XBOOLE_1:63;
{(LMP C)} misses P by A3, Lm6, JORDAN21:44;
hence LSeg (LMP C),|[0 ,(- 3)]| misses P by A4, A6, XBOOLE_1:70; :: thesis: verum