let T be non empty TopSpace; :: thesis: ( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T )
hereby :: thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ) implies T is compact )
assume A1: T is compact ; :: thesis: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T
let F be proper Filter of (BoolePoset ([#] T)); :: thesis: ex x being Point of T st x is_a_cluster_point_of F,T
reconsider G = F as proper Filter of (BoolePoset ([#] T)) ;
consider x being Point of T such that
A2: x is_a_cluster_point_of a_net G by A1, Lm1;
take x = x; :: thesis: x is_a_cluster_point_of F,T
thus x is_a_cluster_point_of F,T by A2, Th16; :: thesis: verum
end;
assume A3: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ; :: thesis: T is compact
now :: thesis: for N being net of T st N in NetUniv T holds
ex x being Point of T st x is_a_cluster_point_of N
let N be net of T; :: thesis: ( N in NetUniv T implies ex x being Point of T st x is_a_cluster_point_of N )
assume N in NetUniv T ; :: thesis: ex x being Point of T st x is_a_cluster_point_of N
reconsider F = a_filter N as proper Filter of (BoolePoset the carrier of T) ;
consider x being Point of T such that
A4: x is_a_cluster_point_of F,T by A3;
take x = x; :: thesis: x is_a_cluster_point_of N
thus x is_a_cluster_point_of N by A4, Th11; :: thesis: verum
end;
hence T is compact by Lm2; :: thesis: verum