proposition: Lemma top_element_maximal : forall a b x : E, is_top_element a b x -> is_maximal a b x.
proof: Proof. intros. unfold is_top_element in H. unfold is_upper_bound in H. unfold is_maximal in |- *. ee. intros. am. am. am. ir. ufi axioms H; ee. ap H8. am. ap H3; am. Qed.
imports: universe