proposition: Lemma linear_minimal_bottom_element : forall a b x : E, is_linear a -> is_minimal a b x -> is_bottom_element a b x.
proof: Proof. intros. unfold is_linear in H. unfold is_minimal in H0. unfold is_bottom_element in |- *. unfold is_lower_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. unfold axioms in H; xe. assert (y = x). apply H4; au. rewrite H9. unfold axioms in H; ee. ap H. am. Qed.
imports: universe