let p be Point of (TOP-REAL 2); :: thesis: for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D & p in LSeg ((LMP D),|[0,(- 3)]|) holds
p `2 <= (LMP D) `2
let D be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in D & p in LSeg ((LMP D),|[0,(- 3)]|) implies p `2 <= (LMP D) `2 )
set x = LMP D;
assume that
A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in D and
A2: p in LSeg ((LMP D),|[0,(- 3)]|) ; :: thesis: p `2 <= (LMP D) `2
A3: LMP D in LSeg ((LMP D),|[0,(- 3)]|) by RLTOPSP1:68;
A4: LSeg ((LMP D),|[0,(- 3)]|) is vertical by A1, Th82;
A5: |[0,(- 3)]| = |[(|[0,(- 3)]| `1),(|[0,(- 3)]| `2)]| by EUCLID:53;
A6: LMP D = |[((LMP D) `1),((LMP D) `2)]| by EUCLID:53;
|[0,(- 3)]| in LSeg ((LMP D),|[0,(- 3)]|) by RLTOPSP1:68;
then A7: |[0,(- 3)]| `1 = (LMP D) `1 by A3, A4;
|[0,(- 3)]| `2 <= (LMP D) `2 by A1, Lm23, Th84, JORDAN21:31;
hence p `2 <= (LMP D) `2 by A2, A5, A6, A7, JGRAPH_6:1; :: thesis: verum