theorem Th14: :: WAYBEL33:14

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