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