let L be LATTICE; :: thesis: ( L is completely-distributive implies L is Heyting )
assume L is completely-distributive ; :: thesis: L is Heyting
then reconsider L = L as completely-distributive LATTICE ;
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L by Th26;
then for x being Element of L holds x "/\" is lower_adjoint by WAYBEL_1:67;
hence L is Heyting by WAYBEL_1:def 19; :: thesis: verum