proposition: Lemma ordinal_container : forall z:E, (forall u:E, inc u z -> is_ordinal u) -> exists o:E, (is_ordinal o & sub z o).
proof: Proof. ir. pose (q:= (union z)). assert (is_ordinal q). uf q; ap ordinal_union; am. sh (tack_on q q). ee. ap ordinal_tack_on; am. uhg; ir. assert (ordinal_leq x q). uhg; ee. ap H; am. am. uhg; ir. uf q; apply union_inc with x. am. am. wr ordinal_leq_inc_tack_on. am. am. Qed.
imports: Arith transfinite