theorem :: SPPOL_1:6

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )