for L being complete LATTICE
for X, Y being set st X c= Y holds
( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )