Section Sets.

  Variable A : Type.

  Definition set : Type := A → Prop.

  Definition empty_set : set := fun _ ⇒ False.

  Definition full_set : set := fun _ ⇒ True.

  Definition is_full_set(P : set) : Prop := ∀(a : A), P a.

  Definition add(a : A)(P : set) : set := fun(b : A) ⇒ a = b ∨ P b.

  Definition subset(P Q : set) : Prop := ∀(a : A), P a → Q a.

  Definition union(P Q : set) : set := fun(a : A) ⇒ P a ∨ Q a.

  Definition intersection(P Q : set) : set := fun(a : A) ⇒ P a ∧ Q a.

  Definition set_inverse(P : set) : set := fun(a : A) ⇒ ¬ (P a).

  Lemma subset_refl : ∀(P : set), subset P P.

  Lemma subset_trans : ∀(P1 P2 P3 : set),
    subset P1 P2 → subset P2 P3 → subset P1 P3.

  Lemma subset_add : ∀(P : set)(a : A), subset P (add a P).

  Lemma subset_union_left : ∀(P Q : set), subset P (union P Q).

  Lemma subset_union_right : ∀(P Q : set), subset Q (union P Q).

  Lemma subset_union_both : ∀(P1 P2 Q1 Q2 : set),
    subset P1 Q1 → subset P2 Q2 → subset (union P1 P2) (union Q1 Q2).

  Lemma subset_union_lub : ∀(P1 P2 Q : set),
    subset P1 Q → subset P2 Q → subset (union P1 P2) Q.

  Definition set_equal(P Q : set) : Prop :=
    ∀(a : A), P a ↔ Q a.

  Lemma set_equal_refl : ∀(P : set), set_equal P P.

  Lemma set_equal_symm : ∀(P Q : set),
    set_equal Q P → set_equal P Q.

  Lemma set_equal_trans : ∀(P1 P2 P3 : set),
    set_equal P1 P2 → set_equal P2 P3 → set_equal P1 P3.

  Lemma set_equal_subset_char : ∀(P Q : set),
    set_equal P Q ↔ (subset P Q ∧ subset Q P).

  Lemma set_equal_subset : ∀(P1 P2 : set)(Q1 Q2 : set),
    set_equal P1 P2 →
    set_equal Q1 Q2 →
    subset P1 Q1 →
      subset P2 Q2.

  Lemma union_comm : ∀(P Q : set),
    set_equal (union P Q) (union Q P).

  Lemma set_equal_union : ∀(P1 P2 Q1 Q2 : set),
    set_equal P1 Q1 →
    set_equal P2 Q2 →
      set_equal (union P1 P2) (union Q1 Q2).

  Lemma set_equal_intersection : ∀(P1 P2 Q1 Q2 : set),
    set_equal P1 Q1 →
    set_equal P2 Q2 →
      set_equal (intersection P1 P2) (intersection Q1 Q2).

  Lemma set_equal_set_inverse : ∀(P Q : set),
    set_equal P Q → set_equal (set_inverse P) (set_inverse Q).

  Lemma set_equal_is_full : ∀(P Q : set),
    set_equal P Q →
    is_full_set P →
      is_full_set Q.

  Lemma set_equal_union_subset_right : ∀(P Q : set),
    subset Q P → set_equal (union P Q) P.

  Lemma subset_empty_set : ∀(P : set), subset empty_set P.

  Lemma set_equal_union_empty_right : ∀(P Q : set),
    set_equal Q empty_set → set_equal (union P Q) P.

  Lemma set_equal_implies_subset : ∀(P Q : set),
    set_equal P Q → subset P Q.

  Lemma set_equal_rw_r : ∀(P1 P2 P3 : set),
    set_equal P2 P3 → set_equal P1 P3 → set_equal P1 P2.

  Lemma intersection_complement : ∀(P : set)(a : A),
    not (intersection P (set_inverse P) a).

  Lemma set_inverse_intersection : ∀(P Q : set)(a : A),
    union (set_inverse P) (set_inverse Q) a →
      set_inverse (intersection P Q) a.

  Lemma double_set_inverse : ∀(P : set)(a : A),
    P a → set_inverse (set_inverse P) a.

  Lemma full_set_full : is_full_set full_set.

  Lemma full_subset_full :
    ∀(P : set), subset full_set P → is_full_set P.

End Sets.

Implicit Arguments is_full_set [A].
Implicit Arguments add [A].
Implicit Arguments subset [A].
Implicit Arguments union [A].
Implicit Arguments intersection [[A]].
Implicit Arguments set_inverse [[A]].
Implicit Arguments set_equal [A].

Definition sets_containing{A : Type}(a : A) : set (set A) :=
  fun(s : set A) ⇒ s a.