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 |[0 ,3]|,(UMP D) c= north_halfline (UMP D) )
set p = UMP D;
assume A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in D ; :: thesis: LSeg |[0 ,3]|,(UMP D) c= north_halfline (UMP D)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg |[0 ,3]|,(UMP D) or x in north_halfline (UMP D) )
assume A2: x in LSeg |[0 ,3]|,(UMP D) ; :: thesis: x in north_halfline (UMP D)
then reconsider x = x as Point of (TOP-REAL 2) ;
A3: UMP D in LSeg |[0 ,3]|,(UMP D) by RLTOPSP1:69;
LSeg |[0 ,3]|,(UMP D) is vertical by A1, Th81;
then A4: x `1 = (UMP D) `1 by A2, A3, SPPOL_1:def 3;
(UMP D) `2 <= x `2 by A1, A2, Th85;
hence x in north_halfline (UMP D) by A4, TOPREAL1:def 12; :: thesis: verum