let S be non empty TopSpace; :: thesis: for c being Point of S
for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let c be Point of S; :: thesis: for N being net of S
for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let N be net of S; :: thesis: for A being Subset of S st c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A holds
c in A
let A be Subset of S; :: thesis: ( c is_a_cluster_point_of N & A is closed & rng the mapping of N c= A implies c in A )
assume that
A1: c is_a_cluster_point_of N and
A2: A is closed and
A3: rng the mapping of N c= A ; :: thesis: c in A
consider M being subnet of N such that
A4: c in Lim M by A1, Th32;
reconsider R = rng the mapping of M as Subset of S ;
ex f being Function of M,N st
( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) ) by YELLOW_6:def 9;
then R c= rng the mapping of N by RELAT_1:26;
then R c= A by A3;
then A5: Cl R c= Cl A by PRE_TOPC:19;
c in Cl R by A4, Th24;
then c in Cl A by A5;
hence c in A by A2, PRE_TOPC:22; :: thesis: verum