let L be Semilattice; :: thesis: for F being Filter of L
for G being GeneratorSet of F
for f, g being Function of NAT ,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 Function of NAT ,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 Function of NAT ,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 Function of NAT ,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: g . 0 in rng g by FUNCT_2:6;
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 set such that
A5: n in dom g and
A6: g . n = a by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A5;
reconsider Y = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1;
A7: Y c= G

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Y or q in G )
assume q in Y ; :: thesis: q in G
then consider m being Element of NAT such that
A8: q = f . m and
m <= n ;
dom f = NAT by FUNCT_2:def 1;
hence q in G by A1, A8, FUNCT_1:def 5; :: thesis: verum

end;

G c= F by Lm4;
then Y c= F by A7, XBOOLE_1:1;
then A9: "/\" 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 A6, A9; :: thesis: verum

end;

hence rng g is GeneratorSet of F by A3, A1, A2, Th35, Th34; :: thesis: verum