proposition: Lemma compl_comp_rev : forall A B : part_set E, Equal (compl A) (compl B) -> Equal A B.
proof: Proof. simpl in |- *; auto with algebra. unfold eq_part in |- *; auto with algebra. simpl in |- *; unfold not in |- *. intros A B H' x; try assumption. elim (H' x). apply NNPP. tauto. Qed.
imports: Classical_Prop Parts