proposition: Lemma le_cardinal_antisym: forall kappa lambda:Cardinal, le_cardinal kappa lambda -> le_cardinal lambda kappa -> eq_cardinal kappa lambda.
proof: Proof. intros. destruct H. inversion H0. destruct H1. destruct H2. pose proof (CSB Y0 X0 f f0 H H3). destruct H1. exists x. assumption. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec