proposition: Lemma card_isomorphic : forall x, are_isomorphic x (cardinality x).
proof: Proof. ir. uf cardinality. ap sow_property. cp (every_set_can_be_well_ordered x). nin H. ee. sh (wo_ordinal x0). ee. ap wo_ordinal_is_ordinal. am. apply trans_bij_isomorphic with (wo_avatar x0). wr H0. ap wo_avatar_bijective. am. Qed.
imports: Arith ordinal