theorem Th45: :: LATTICE3:45

for C being complete Lattice
for X, Y being set st X c= Y holds
( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) )