Definition complement_bottom_axiom (x : X) (y : complement x) : x ⊗ y = ⊥ := dirprod_pr2 (pr2 y).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.