proposition: Lemma ordinal_saturated : forall a b c, is_ordinal c -> inc b c -> ordinal_leq a b -> inc a c.
proof: Proof. ir. assert (ordinal_lt a c). uhg; ee. uhg; ee. lu. am. uh H1. ee. rwi ordinal_inc_rw H0. ee. uh H4. ee. apply sub_trans with b; am. am. uhg; ir. uh H1; ee. rwi H2 H4. apply ordinal_not_inc_itself with b. am. ap H4; am. rwi ordinal_lt_rw H2. ee; am. Qed.
imports: Arith transfinite