for p, q being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(q `1),(p `2)]|,q*> holds
( f /. 1 = p & f /. (len f) = q & f is being_S-Seq )