:: deftheorem defines lim_inf WAYBEL33:def 1 :
for L being non empty Poset
for X being non empty Subset of L
for F being Filter of (BoolePoset X) holds lim_inf F = "\/" ( { (inf B) where B is Subset of L : B in F } ,L);