theorem Th24: :: SPPOL_2:24

for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st q in rng f holds
L~ f = (L~ (f -: q)) \/ (L~ (f :- q))