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 object ; :: 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:68;
LSeg (|[0,3]|,(UMP D)) is vertical by A1, Th81;
then A4: x `1 = (UMP D) `1 by A2, A3;
(UMP D) `2 <= x `2 by A1, A2, Th85;
hence x in north_halfline (UMP D) by A4, TOPREAL1:def 10; :: thesis: verum