let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x << y implies for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume A1: x << y ; :: thesis: for F being ultra Filter of (BoolePoset the carrier of T) st x in F holds
ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
let F be ultra Filter of (BoolePoset the carrier of T); :: thesis: ( x in F implies ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T ) )
assume x in F ; :: thesis: ex p being Element of T st
( p in y & p is_a_convergence_point_of F,T )
then consider p being Element of T such that
A2: ( p in y & p is_a_cluster_point_of F,T ) by A1, Th32;
take p ; :: thesis: ( p in y & p is_a_convergence_point_of F,T )
thus ( p in y & p is_a_convergence_point_of F,T ) by A2, Th31; :: thesis: verum