proposition: Lemma Complement_Complement : forall A:Ensemble U, Complement U (Complement U A) = A.
proof: Proof. unfold Complement; intros; apply Extensionality_Ensembles; auto with sets. red; split; auto with sets. red; intros; apply NNPP; auto with sets. Qed.
imports: Ensembles Constructive_sets Classical