for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2) by RLTOPSP1:68, Th7;