let L be Semilattice; 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; 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; 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; ( 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)
; rng g is GeneratorSet of F
A3:
rng g is_coarser_than F
g . 0 in rng g
by FUNCT_2:4;
hence
rng g is GeneratorSet of F
by A1, A2, A3, Th30, Th31; verum