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 that
A2: ( A is open & p in A ) and
A3: not A in F ; :: thesis: contradiction
F is prime by Th22;
then the carrier of T \ A in F by A3, Th21;
then A meets the carrier of T \ A by A1, A2;
hence contradiction by XBOOLE_1:79; :: thesis: verum
end;
assume A4: 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 A5: A in F by A4;
Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18;
then A6: not {} in F by Th4;
let B be set ; :: thesis: ( B in F implies A meets B )
assume A7: B in F ; :: thesis: A meets B
then reconsider a = A, b = B as Element of (BoolePoset the carrier of T) by A5;
a "/\" b = A /\ B by YELLOW_1:17;
then A /\ B in F by A5, A7, WAYBEL_0:41;
hence A meets B by A6; :: thesis: verum