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:64;
hence L is Heyting by WAYBEL_1:def 19; :: thesis: verum