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

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