let L be Semilattice; :: thesis: for F being Filter of L
for G being GeneratorSet of F
for f, g being sequence of the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds
rng g is GeneratorSet of F
let F be Filter of L; :: thesis: for G being GeneratorSet of F
for f, g being sequence of the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds
rng g is GeneratorSet of F
let G be GeneratorSet of F; :: thesis: for f, g being sequence of the carrier of L st rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds
rng g is GeneratorSet of F
let f, g be sequence of the carrier of L; :: thesis: ( rng f = G & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies rng g is GeneratorSet of F )
assume that
A1: rng f = G and
A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; :: thesis: rng g is GeneratorSet of F
A3: rng g is_coarser_than F

proof

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in rng g or ex b₁ being Element of the carrier of L st
( b₁ in F & b₁ <= a ) )
assume a in rng g ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in F & b₁ <= a )
then consider n being object such that
A4: n in dom g and
A5: g . n = a by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A4;
reconsider Y = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1;
A6: Y c= G

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Y or q in G )
assume q in Y ; :: thesis: q in G
then A7: ex m being Element of NAT st
( q = f . m & m <= n ) ;
dom f = NAT by FUNCT_2:def 1;
hence q in G by A1, A7, FUNCT_1:def 3; :: thesis: verum

end;

G c= F by Lm4;
then Y c= F by A6;
then A8: "/\" (Y,L) in F by WAYBEL_0:43;
g . n = "/\" (Y,L) by A2;
hence ex b being Element of L st
( b in F & b <= a ) by A5, A8; :: thesis: verum

end;

g . 0 in rng g by FUNCT_2:4;
hence rng g is GeneratorSet of F by A1, A2, A3, Th30, Th31; :: thesis: verum