proposition: Proposition bottom_element_eq {X : hSet} (RX : PartialOrder X) (b₁ b₂ : bottom_element RX) : b₁ = b₂.
proof: Proof. use subtypePath. { intro. use impred ; intro. apply propproperty. } use (antisymm_PartialOrder RX). - apply b₁. - apply b₂. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions