theorem Th13: :: WAYBEL33:13

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