for C being complete Lattice
for X, Y being set st ( for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ) holds
"\/" (X,C) [= "\/" (Y,C)