let L be lower-bounded continuous LATTICE; :: thesis: ( L is distributive iff L is Heyting )
thus ( L is distributive implies L is Heyting ) :: thesis: ( L is Heyting implies L is distributive )

proof

assume L is distributive ; :: thesis: L is Heyting
then PRIME L is order-generating by Th35;
then ( L is distributive & L is meet-continuous ) by Th34;
hence L is Heyting ; :: thesis: verum

end;

thus ( L is Heyting implies L is distributive ) ; :: thesis: verum