theorem Th25: :: SPPOL_2:25

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for n being Nat st p in LSeg (f,n) holds
L~ f = L~ (Ins (f,n,p))