theorem Th63: :: WAYBEL_1:63

for S being Semilattice st ( for x being Element of S holds x "/\" is lower_adjoint ) holds
for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)