proposition: Proposition trans_abstract_basis {B : abstract_basis} {b₁ b₂ b₃ : B} (p : b₁ ≺ b₂) (q : b₂ ≺ b₃) : b₁ ≺ b₃.
proof: Proof. exact (pr12 B b₁ b₂ b₃ p q). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions