let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in rng f holds
L~ (f :- p) c= L~ f
let p be Point of (TOP-REAL 2); :: thesis: ( p in rng f implies L~ (f :- p) c= L~ f )
assume p in rng f ; :: thesis: L~ (f :- p) c= L~ f
then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24;
hence L~ (f :- p) c= L~ f by XBOOLE_1:7; :: thesis: verum