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