let T be non empty TopStruct ; :: thesis: for S being sequence of T
for S1 being subsequence of S holds Lim S c= Lim S1
let S be sequence of T; :: thesis: for S1 being subsequence of S holds Lim S c= Lim S1
let S1 be subsequence of S; :: thesis: Lim S c= Lim S1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim S or x in Lim S1 )
assume A1: x in Lim S ; :: thesis: x in Lim S1
then reconsider x9 = x as Point of T ;
S is_convergent_to x9 by A1, FRECHET:def 5;
then S1 is_convergent_to x9 by Th15;
hence x in Lim S1 by FRECHET:def 5; :: thesis: verum