proposition: Lemma emptyset_ordinal : is_ordinal emptyset.
proof: Proof. assert (emptyset = union emptyset :> E). ap extensionality; uhg; ir. elim (B H). cp (union_exists H). nin H0. ee. elim (B H1). rw H. ap ordinal_union; ir. elim (B H0). Qed.
imports: Arith transfinite