proposition: Lemma ordinal_inc_rw : forall x o:E, is_ordinal o -> (inc x o = (is_ordinal x & strict_sub x o)).
proof: Proof. ir. ap iff_eq; ir. dj. apply ordinal_inc_ordinal with o; am. uhg; ee. uhg; uhg; ir. apply ordinal_not_inc_itself with o. am. rwi H2 H0. am. nin (ordinal_sub_or H H1). assert (inc x x). ap H2; am. assert False. apply ordinal_not_inc_itself with x; am. elim H4. am. ee. ap ordinal_strict_sub_inc; am. Qed.
imports: Arith transfinite