theorem :: SPPOL_1:12

for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg (p1,p2) by Th11;