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

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

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

g . 0 in rng g
by FUNCT_2:4;
let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in rng g or ex b_{1} being Element of the carrier of L st

( b_{1} in F & b_{1} <= a ) )

assume a in rng g ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in F & b_{1} <= 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

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;( b

assume a in rng g ; :: thesis: ex b

( b

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

G c= F
by Lm4;
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;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

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

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