theorem Th32: :: WAYBEL12:32

for L being 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