theorem Th1: :: WAYBEL11:1

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