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