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 } ;
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:2;
then A1: the carrier of L in UN by CLASSES1:3, CLASSES1:52;
then bool the carrier of L in UN by CLASSES2:59;
then A2: [: the carrier of L,(bool the carrier of L):] in UN by A1, CLASSES2:61;
{ [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;
then ( { [a,f] where a is Element of L, f is Element of F : a in f } = the carrier of (a_net F) & { [a,f] where a is Element of L, f is Element of F : a in f } in UN ) by A2, CLASSES1:def 1, YELLOW19:def 4;
hence a_net F in NetUniv L by YELLOW_6:def 11; :: thesis: verum