ABSTRACT: We show that every finitely presented Heyting algebra is a bi-Heyting algebra, i.e., there is an operation `suplement' defined dual to the notion of implication. Our main technique is algebraic: We use a filtration of a given (f.p.) Heyting algebras by finite distributive lattices. This allows as well to characterize minimal and maximal join-irreducible elements and thus gives yet another proof of the disjunction property of intuitionistic propositional logic. Although not part of this talk it is worthwhile to note that the class of Heyting algebras that are bi-Heyting is much much larger: It includes all (!) free Heyting algebras. References: C. Butz. Finitely presented Heyting algebras. Preprint. Available as http://www.brics.dk/~butz/heyting.ps.gz. S. Ghilardi. Free Heyting algebras as bi-Heyting algebras. C. R. Math. Rep. Acad. Sci. Canada, 14:240-244, 1992. (Proves that Heyting algebras free on a _finite_ set of generators are bi-Heyting.) S. Ghilardi and M. Zawadowski. A sheaf representation and duality for finitely presented Heyting algebras. J. Symbolic Logic 60:911--939, 1995.