proposition: Lemma ordinal_not_inc : forall x o:E, is_ordinal o -> inc x o -> ~inc x x.
proof: Proof. ir. util (ordinal_induction (p:= fun y:E=>(forall u:E, inc u y -> ~inc u u))). ir. cp (union_exists H2). nin H3; ee. cp (H1 x0 H4 u H3). am. ir. rwi tack_on_inc H2; nin H2. ap H1; am. uhg; ir. util (H1 u0). wr H2; am. ap H4; am. cbv beta in H1. apply H1 with o. am. am. Qed.
imports: Arith transfinite