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

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