theorem Th20: :: SPPOL_2:20

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st not f is empty holds
L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)