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

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

hence
T is compact
by Lm2; :: thesis: verumex 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;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