let H be non empty RelStr ; :: thesis: ( H is Heyting implies H is distributive )
assume that
A1: H is LATTICE and
A2: for x being Element of H holds x "/\" is lower_adjoint ; :: according to WAYBEL_1:def 19 :: thesis: H is distributive
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 A1, A2, Th66;
hence H is distributive by A1, Th68; :: thesis: verum