theorem Th28: :: JORDAN2C:41

for n being Nat
for w1, w2 being Point of (TOP-REAL n)
for P being Subset of (TopSpaceMetr (Euclid n)) st P = LSeg (w1,w2) & not 0. (TOP-REAL n) in LSeg (w1,w2) holds
ex w0 being Point of (TOP-REAL n) st
( w0 in LSeg (w1,w2) & |.w0.| > 0 & |.w0.| = (dist_min P) . (0. (TOP-REAL n)) )