let H be non empty RelStr ; :: thesis: ( H is Heyting implies H is distributive )
assume A1: ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) ; :: according to WAYBEL_1:def 19 :: thesis: H is distributive
then for X being Subset of H st ex_sup_of X,H holds
for x being Element of H holds x "/\" ("\/" X,H) = "\/" { (x "/\" y) where y is Element of H : y in X } ,H by Th66;
hence H is distributive by A1, Th68; :: thesis: verum