let L be Semilattice; :: thesis: for F being Filter of L

for G being GeneratorSet of F holds G c= F

let F be Filter of L; :: thesis: for G being GeneratorSet of F holds G c= F

let G be GeneratorSet of F; :: thesis: G c= F

F = uparrow (fininfs G) by Def3;

hence G c= F by WAYBEL_0:62; :: thesis: verum

for G being GeneratorSet of F holds G c= F

let F be Filter of L; :: thesis: for G being GeneratorSet of F holds G c= F

let G be GeneratorSet of F; :: thesis: G c= F

F = uparrow (fininfs G) by Def3;

hence G c= F by WAYBEL_0:62; :: thesis: verum