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 |[0 ,3]|,(UMP D) holds
(UMP D) `2 <= p `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 |[0 ,3]|,(UMP D) implies (UMP D) `2 <= p `2 )
set x = UMP D;
assume that
A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D and
A2: p in LSeg |[0 ,3]|,(UMP D) ; :: thesis: (UMP D) `2 <= p `2
A3: UMP D in LSeg |[0 ,3]|,(UMP D) by RLTOPSP1:69;
A4: LSeg |[0 ,3]|,(UMP D) is vertical by A1, Th81;
A5: |[0 ,3]| = |[(|[0 ,3]| `1 ),(|[0 ,3]| `2 )]| by EUCLID:57;
A6: UMP D = |[((UMP D) `1 ),((UMP D) `2 )]| by EUCLID:57;
|[0 ,3]| in LSeg |[0 ,3]|,(UMP D) by RLTOPSP1:69;
then A7: |[0 ,3]| `1 = (UMP D) `1 by A3, A4, SPPOL_1:def 3;
(UMP D) `2 <= |[0 ,3]| `2 by A1, Lm21, Th83, JORDAN21:43;
hence (UMP D) `2 <= p `2 by A2, A5, A6, A7, JGRAPH_6:9; :: thesis: verum