let T be non empty TopSpace; :: thesis: for A being Subset of T 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 T; :: 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 :: thesis: verum
proof
reconsider A = A as Subset of T ;
reconsider L = Lim S as Subset of T ;
L c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in L or y in A )
assume A3: y in L ; :: thesis: y in A
then reconsider p = y as Point of T ;
A4: S is_convergent_to p by A3, Def5;
for U1 being Subset of T st U1 is open & p in U1 holds
A meets U1
proof
let U1 be Subset of T; :: thesis: ( U1 is open & p in U1 implies A meets U1 )
assume A5: U1 is open ; :: thesis: ( not p in U1 or A meets U1 )
reconsider U2 = U1 as Subset of T ;
assume p in U1 ; :: thesis: A meets U1
then consider n being Nat such that
A6: for m being Nat st n <= m holds
S . m in U2 by A4, A5;
A7: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then A8: S . n in rng S by FUNCT_1:def 3, A7;
S . n in U1 by A6;
then S . n in A /\ U1 by A2, A8, XBOOLE_0:def 4;
hence A meets U1 ; :: thesis: verum
end;
then p in Cl A by PRE_TOPC:def 7;
hence y in A by A1, PRE_TOPC:22; :: thesis: verum
end;
hence Lim S c= A ; :: thesis: verum
end;