for L being Semilattice
for A being Subset of L
for B being non empty Subset of L st A is_coarser_than B holds
fininfs A is_coarser_than fininfs B