proposition: Lemma iso_sub_ordinal_leq : forall u o, is_ordinal o -> iso_sub u o -> ordinal_leq (cardinality u) o.
proof: Proof. ir. uh H0. nin H0. ee. cp (cardinality_invariant H0). rw H2. ap subset_ordinal_cardinal_leq. am. am. Qed.
imports: Arith ordinal