let L be complete lim-inf TopLattice; :: thesis: for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L
let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F is_a_convergence_point_of F,L
set x = lim_inf F;
let A be Subset of L; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not lim_inf F in A or A in F )
assume A1: ( A is open & lim_inf F in A & not A in F ) ; :: thesis: contradiction
F is prime by WAYBEL_7:26;
then A2: ([#] L) \ A in F by A1, WAYBEL_7:25;
then ( A ` <> {} & A ` is closed ) by A1, YELLOW19:2;
then lim_inf F in A ` by A2, Th18;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum