theorem Th65: :: WAYBEL_1:65

for S being LATTICE st ( 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) ) holds
S is distributive