let T be non empty TopSpace; :: thesis: for F being ultra Filter of (BoolePoset the carrier of T)
for p being set holds
( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
set L = BoolePoset the carrier of T;
let F be ultra Filter of (BoolePoset the carrier of T); :: thesis: for p being set holds
( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
let p be set ; :: thesis: ( p is_a_cluster_point_of F,T iff p is_a_convergence_point_of F,T )
thus ( p is_a_cluster_point_of F,T implies p is_a_convergence_point_of F,T ) :: thesis: ( p is_a_convergence_point_of F,T implies p is_a_cluster_point_of F,T )

proof

assume A1: for A being Subset of T st A is open & p in A holds
for B being set st B in F holds
A meets B ; :: according to WAYBEL_7:def 4 :: thesis: p is_a_convergence_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( A is open & p in A implies A in F )
assume A2: ( A is open & p in A & not A in F ) ; :: thesis: contradiction
F is prime by Th26;
then the carrier of T \ A in F by A2, Th25;
then ( A meets the carrier of T \ A & A misses the carrier of T \ A ) by A1, A2, XBOOLE_1:79;
hence contradiction ; :: thesis: verum

end;

assume A3: for A being Subset of T st A is open & p in A holds
A in F ; :: according to WAYBEL_7:def 5 :: thesis: p is_a_cluster_point_of F,T
let A be Subset of T; :: according to WAYBEL_7:def 4 :: thesis: ( A is open & p in A implies for B being set st B in F holds
A meets B )
assume ( A is open & p in A ) ; :: thesis: for B being set st B in F holds
A meets B
then A4: A in F by A3;
let B be set ; :: thesis: ( B in F implies A meets B )
assume A5: B in F ; :: thesis: A meets B
then reconsider a = A, b = B as Element of (BoolePoset the carrier of T) by A4;
( a "/\" b = A /\ B & Bottom (BoolePoset the carrier of T) = {} ) by YELLOW_1:17, YELLOW_1:18;
then ( A /\ B in F & not {} in F ) by A4, A5, Th8, WAYBEL_0:41;
hence A meets B by XBOOLE_0:def 7; :: thesis: verum