proposition: Lemma compl_compl : forall A : part_set E, Equal (compl (compl A)) A.
proof: Proof. simpl in |- *; auto with algebra. unfold eq_part in |- *; auto with algebra. simpl in |- *; unfold not in |- *. intros A x; try assumption. split; [ try assumption | idtac ]. apply NNPP. tauto. Qed.
imports: Classical_Prop Parts