proposition: Lemma empty_included : forall A : part_set E, included (empty E) A.
proof: Proof. simpl in |- *; unfold included in |- *; auto with algebra. intros A x H'; try assumption. absurd (in_part x (empty E)); auto with algebra. Qed.
imports: Sets