Lemma 1.4.11. The Lindenbaum-Tarski algebra of any theory relative to IPC is a Heyting algebra.