proposition: Lemma wo_subset_choose_bottom : forall a b : E, is_wo_subset a b -> nonempty b -> is_bottom_element a b (choose_bottom_element a b).
proof: Proof. ir. assert (ex (fun x : E => is_bottom_element a b x)). uh H. ee. uh H1; ee. assert (sub b (U (suborder b a))). rw underlying_suborder. uf sub; ir; am. cp (H2 b H3 H0). nin H4. sh x. uhg. ee. uhg; ee. uh H. ee; am. uh H; ee; am. uh H4; ee. uh H; ee. ap H6; am. ir. uh H4; ee. uh H4; ee. cp (H9 y H5). rwi leq_suborder_all H10; ee. am. uh H; ee; am. uh H; ee; am. uh H4; ee. am. cp (choose_pr H1). exact H2. Qed.
imports: universe