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

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

end;reconsider L = Lim S as Subset of T ;

L c= A

proof

hence
Lim S c= A
; :: thesis: verum
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

hence y in A by A1, PRE_TOPC:22; :: thesis: verum

end;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

then
p in Cl A
by PRE_TOPC:def 7;
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;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

hence y in A by A1, PRE_TOPC:22; :: thesis: verum