theorem Th61: :: SPRECT_2:61

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