let T be non empty TopSpace; :: thesis: for A being Subset of st A is closed holds
for S being sequence of T st rng S c= A holds
Lim S c= A
let A be Subset of ; :: thesis: ( A is closed implies for S being sequence of T st rng S c= A holds
Lim S c= A )
assume A1: A is closed ; :: thesis: for S being sequence of T st rng S c= A holds
Lim S c= A
let S be sequence of T; :: thesis: ( rng S c= A implies Lim S c= A )
assume A2: rng S c= A ; :: thesis: Lim S c= A
thus Lim S c= A by A1, A2, FRECHET:26; :: thesis: verum