theorem Th16: :: WAYBEL33:16

for L being complete LATTICE
for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M