Proposition cha_basis_antimonotone {H : complete_heyting_algebra} (B : cha_basis H) {b₁ b₂ : B} (p : cha_basis_rel b₁ b₂) : cha_basis_incl b₂ ≤ cha_basis_incl b₁. Proof. exact (pr222 B b₁ b₂ p). 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.