proposition: Lemma linear_maximal_top_element : forall a b x : E, is_linear a -> is_maximal a b x -> is_top_element a b x.
proof: Proof. intros. unfold is_linear in H. unfold is_maximal in H0. unfold is_top_element in |- *. unfold is_upper_bound in |- *. xd. intros. assert (inc x (U a)). apply H1; au. assert (inc y (U a)). apply H1; au. pose (H2 _ _ H6 H7). induction o. uh H. ee. assert (x = y). apply H4; au. rewrite H13. ap H; am. am. Qed.
imports: universe