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