proposition: Lemma bottom_element_minimal : forall a b x : E, is_bottom_element a b x -> is_minimal a b x.
proof: Proof. intros. unfold is_bottom_element in H. unfold is_lower_bound in H. unfold is_minimal in |- *. xe. intros. unfold axioms in H; xe. ap H8. am. ap H3. am. Qed.
imports: universe