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 )

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

proof

thus
( L is Heyting implies L is distributive )
; :: thesis: verum
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;then PRIME L is order-generating by Th35;

then ( L is distributive & L is meet-continuous ) by Th34;

hence L is Heyting ; :: thesis: verum