let D be compact with_the_max_arc Subset of (TOP-REAL 2); ( |[(- 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
; LSeg ((LMP D),|[0,(- 3)]|) c= south_halfline (LMP D)
let x be object ; TARSKI:def 3 ( not x in LSeg ((LMP D),|[0,(- 3)]|) or x in south_halfline (LMP D) )
assume A2:
x in LSeg ((LMP D),|[0,(- 3)]|)
; 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:68;
A4:
LSeg ((LMP D),|[0,(- 3)]|) is vertical
by A1, Th82;
then A5:
x `1 = (LMP D) `1
by A2, A3;
A6:
|[0,(- 3)]| = |[(|[0,(- 3)]| `1),(|[0,(- 3)]| `2)]|
by EUCLID:53;
A7:
LMP D = |[((LMP D) `1),((LMP D) `2)]|
by EUCLID:53;
|[0,(- 3)]| in LSeg ((LMP D),|[0,(- 3)]|)
by RLTOPSP1:68;
then A8:
|[0,(- 3)]| `1 = (LMP D) `1
by A3, A4;
|[0,(- 3)]| `2 <= (LMP D) `2
by A1, Lm23, Th84, JORDAN21:31;
then
x `2 <= (LMP D) `2
by A2, A6, A7, A8, JGRAPH_6:1;
hence
x in south_halfline (LMP D)
by A5, TOPREAL1:def 12; verum