theorem :: WAYBEL_1:64

for S being non empty complete Poset holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )