theorem :: SPRECT_3:16

for g being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st g /. 1 <> p & ( (g /. 1) `1 = p `1 or (g /. 1) `2 = p `2 ) & g is being_S-Seq & (LSeg (p,(g /. 1))) /\ (L~ g) = {(g /. 1)} holds
<*p*> ^ g is being_S-Seq