proposition: Lemma cardinals_unbounded: forall kappa:Cardinal, exists lambda:Cardinal, gt_cardinal lambda kappa.
proof: Proof. destruct kappa. exists (cardinality (T->Prop)). red; red; split. exists (@eq T). red; intros. rewrite H. reflexivity. unfold not; intro. inversion H. destruct H0. destruct H2. contradiction (cantor_diag2 _ f). Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec