let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D implies LSeg (LMP D),|[0 ,(- 3)]| c= south_halfline (LMP D) )
set p = LMP D;
assume A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D ; :: thesis: LSeg (LMP D),|[0 ,(- 3)]| c= south_halfline (LMP D)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (LMP D),|[0 ,(- 3)]| or x in south_halfline (LMP D) )
assume A2: x in LSeg (LMP D),|[0 ,(- 3)]| ; :: thesis: x in south_halfline (LMP D)
then reconsider x = x as Point of (TOP-REAL 2) ;
A3: LMP D in LSeg (LMP D),|[0 ,(- 3)]| by RLTOPSP1:69;
A4: LSeg (LMP D),|[0 ,(- 3)]| is vertical by A1, Th82;
then A5: x `1 = (LMP D) `1 by A2, A3, SPPOL_1:def 3;
A6: ( |[0 ,(- 3)]| = |[(|[0 ,(- 3)]| `1 ),(|[0 ,(- 3)]| `2 )]| & LMP D = |[((LMP D) `1 ),((LMP D) `2 )]| ) by EUCLID:57;
|[0 ,(- 3)]| in LSeg (LMP D),|[0 ,(- 3)]| by RLTOPSP1:69;
then A7: |[0 ,(- 3)]| `1 = (LMP D) `1 by A3, A4, SPPOL_1:def 3;
|[0 ,(- 3)]| `2 <= (LMP D) `2 by A1, Lm25, Th84, JORDAN21:44;
then x `2 <= (LMP D) `2 by A2, A6, A7, JGRAPH_6:9;
hence x in south_halfline (LMP D) by A5, TOPREAL1:def 14; :: thesis: verum