for L being complete lim-inf TopLattice
for F being ultra Filter of (BoolePoset ([#] L)) holds lim_inf F is_a_convergence_point_of F,L