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, Th63;
hence H is distributive by A1, Th65; :: thesis: verum