proposition: Lemma bernstein_cantor_schroeder : forall x y, iso_sub x y -> iso_sub y x -> are_isomorphic x y.
proof: Proof. ir. cp (iso_sub_cardinal_leq H). cp (iso_sub_cardinal_leq H0). cp (ordinal_leq_leq_eq H1 H2). cp (card_isomorphic x). cp (card_isomorphic y). ap are_isomorphic_trans. sh (cardinality x). ee; try am. rw H3. ap are_isomorphic_symm. am. Qed.
imports: Arith ordinal