theorem Th48: :: SPPOL_2:48

for p being Point of (TOP-REAL 2)
for i being Nat
for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds
Ins (f,i,p) is being_S-Seq