let L be Semilattice; :: thesis: for A being Subset of L
for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds
A is_coarser_than rng g

let A be Subset of L; :: thesis: for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds
A is_coarser_than rng g

let f, g be sequence of the carrier of L; :: thesis: ( rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies A is_coarser_than rng g )
assume that
A1: rng f = A and
A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; :: thesis:
let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in A or ex b1 being Element of the carrier of L st
( b1 in rng g & b1 <= a ) )

assume a in A ; :: thesis: ex b1 being Element of the carrier of L st
( b1 in rng g & b1 <= a )

then consider n being object such that
A3: n in dom f and
A4: f . n = a by ;
reconsider n = n as Element of NAT by A3;
reconsider T = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1;
take b = "/\" (T,L); :: thesis: ( b in rng g & b <= a )
( dom g = NAT & g . n = b ) by ;
hence b in rng g by FUNCT_1:def 3; :: thesis: b <= a
f . n in T ;
then A5: {(f . n)} c= T by ZFMISC_1:31;
( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55;
then b <= "/\" ({(f . n)},L) by ;
hence b <= a by ; :: thesis: verum