for L being complete LATTICE
for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)