Proposition cha_basis_trans {H : complete_heyting_algebra} (B : cha_basis H) {b₁ b₂ b₃ : B} (p : cha_basis_rel b₁ b₂) (q : cha_basis_rel b₂ b₃) : cha_basis_rel b₁ b₃. Proof. exact (pr12 B b₁ b₂ b₃ p q). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting.