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 )

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

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 A4:
for A being Subset of T st A is open & p in A holds
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;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

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