proposition: Lemma wo_choose_bottom : forall a b : E, is_well_ordered a -> sub b (U a) -> nonempty b -> is_bottom_element a b (choose_bottom_element a b).
proof: Proof. intros. unfold is_well_ordered in H; ee. pose (H2 b H0 H1). pose (choose_pr e). am. Qed.
imports: universe