proposition: Lemma cardinal_1_single : forall A : part_set E, cardinal A 1 -> exists x : E, Equal A (single x).
proof: Proof. intros. inversion H. exists x. apply Trans with (add_part B x); auto with algebra. apply Trans with (add_part (empty E) x); auto with algebra. Qed.
imports: Union Singleton Diff Classical_Prop