let L be complete LATTICE; :: thesis: for F being proper Filter of (BoolePoset ([#] L)) holds a_net F in NetUniv L
let F be proper Filter of (BoolePoset ([#] L)); :: thesis: a_net F in NetUniv L
set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;
A1: { [a,f] where a is Element of L, f is Element of F : a in f } = the carrier of (a_net F) by YELLOW19:def 4;
A2: { [a,f] where a is Element of L, f is Element of F : a in f } c= [:the carrier of L,(bool the carrier of L):] by Lm4;
set UN = the_universe_of the carrier of L;
reconsider UN = the_universe_of the carrier of L as universal set ;
the_transitive-closure_of the carrier of L in UN by CLASSES1:5;
then A3: the carrier of L in UN by CLASSES1:6, CLASSES1:59;
then bool the carrier of L in UN by CLASSES2:65;
then [:the carrier of L,(bool the carrier of L):] in UN by A3, CLASSES2:67;
then { [a,f] where a is Element of L, f is Element of F : a in f } in UN by A2, CLASSES1:def 1;
hence a_net F in NetUniv L by A1, YELLOW_6:def 14; :: thesis: verum