proposition: Lemma ordinal_inc_ordinal : forall x o:E, is_ordinal o -> inc x o -> is_ordinal x.
proof: Proof. ir. util (ordinal_induction (p:= fun y:E=>(is_ordinal y & forall u:E, inc u y -> is_ordinal u))); ir. ee. ap ordinal_union. ir. cp (H1 u H2). ee; am. ir. nin (union_exists H2). ee. cp (H1 x0 H4). ee. ap H6; am. ee. ap ordinal_tack_on; am. ir. rwi tack_on_inc H3; nin H3. ap H2; am. rw H3; am. cbv beta in H1. cp (H1 o H); ee. ap H3; am. Qed.
imports: Arith transfinite