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