let T be non empty TopSpace; :: thesis: for p being Element of T
for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let p be Element of T; :: thesis: for N being net of T st p in Lim N holds
for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let N be net of T; :: thesis: ( p in Lim N implies for S being Subset of T st S = rng the mapping of N holds
p in Cl S )
assume A1: p in Lim N ; :: thesis: for S being Subset of T st S = rng the mapping of N holds
p in Cl S
let S be Subset of T; :: thesis: ( S = rng the mapping of N implies p in Cl S )
assume S = rng the mapping of N ; :: thesis: p in Cl S
then A2: N is_eventually_in S by Th8;
for G being Subset of T st G is open & p in G holds
S meets G

proof

let G be Subset of T; :: thesis: ( G is open & p in G implies S meets G )
assume that
A3: G is open and
A4: p in G ; :: thesis: S meets G
G = Int G by A3, TOPS_1:23;
then reconsider V = G as a_neighborhood of p by A4, CONNSP_2:def 1;
N is_eventually_in V by A1, YELLOW_6:def 15;
hence S meets G by A2, YELLOW_6:17; :: thesis: verum

end;

hence p in Cl S by PRE_TOPC:def 7; :: thesis: verum