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 that
A1: A is open and
A2: lim_inf F in A and
A3: not A in F ; :: thesis: contradiction
F is prime by WAYBEL_7:22;
then A4: ([#] L) \ A in F by A3, WAYBEL_7:21;
then A ` <> {} by YELLOW19:1;
then lim_inf F in A ` by A1, A4, Th18;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum