let D be compact with_the_max_arc Subset of (TOP-REAL 2); ( |[(- 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
; LSeg (|[0,3]|,(UMP D)) c= north_halfline (UMP D)
let x be object ; TARSKI:def 3 ( not x in LSeg (|[0,3]|,(UMP D)) or x in north_halfline (UMP D) )
assume A2:
x in LSeg (|[0,3]|,(UMP D))
; 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; verum