let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being Point of T holds
( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) )
let A be Subset of T; :: thesis: for x being Point of T holds
( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) )
let x be Point of T; :: thesis: ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) )
hereby :: thesis: ( ex F being proper Filter of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T ) implies x in Cl A )
assume x in Cl A ; :: thesis: ex F being Subset of (BoolePoset ([#] T)) st
( A in F & x is_a_cluster_point_of F,T )
then consider N being net of T such that
A1: N is_eventually_in A and
A2: x is_a_cluster_point_of N by Th21;
set F = a_filter N;
take F = a_filter N; :: thesis: ( A in F & x is_a_cluster_point_of F,T )
thus A in F by A1; :: thesis: x is_a_cluster_point_of F,T
thus x is_a_cluster_point_of F,T by A2, Th11; :: thesis: verum
end;
given F being proper Filter of (BoolePoset ([#] T)) such that A3: A in F and
A4: x is_a_cluster_point_of F,T ; :: thesis: x in Cl A
reconsider F9 = F as proper Filter of (BoolePoset ([#] T)) ;
A5: a_filter (a_net F9) = F by Th14;
then A6: x is_a_cluster_point_of a_net F9 by A4, Th11;
a_net F9 is_eventually_in A by A3, A5, Th10;
hence x in Cl A by A6, Th21; :: thesis: verum