theorem Th29: :: SPPOL_2:29

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