proposition: Lemma top_element_unique : forall a b x y : E, is_top_element a b x -> is_top_element a b y -> x = y.
proof: Proof. intros. unfold is_top_element in H, H0; xe. unfold is_upper_bound in H, H0; xe. unfold axioms in H; xe. ap H11. ap H6; am. ap H8; am. Qed.
imports: universe