A = B-(B-A) ⇔ A⊆B

人と人とのコミュニケーションを目的にするので、機械可読ではない。特に、新しい変数（fresh variable）が登場したら、適当な変域の自由変数（または全称束縛変数）と解釈する。

前提

次は前提（既に知っているもの）とする。':⇔' は '⇔' と同じだが、定義していることを示すために':'を付けている。

論理の法則

使いそうなものだけ。

1. (⇔定義) (P⇔Q) :⇔ (P⇒Q)∧(Q⇒P) // '⇔'の定義に'⇔'を使っているというツッコミはあるだろうが、、、
2. (ド・モルガン) ¬(P∧Q) ⇔ ¬P∨¬Q, 　¬(P∨Q) ⇔ ¬P∧¬Q
3. (二重否定) ¬¬P ⇔ P
4. (分配) P∧(Q∨R) ⇔ (P∧Q)∨(P∧Q), 　P∨(Q∧R) ⇔ (P∨Q)∧(P∨Q)
5. (矛盾) P∧¬P ⇔ false
6. (∧単位) true∧P ⇔ P
7. (∧交換) P∧Q ⇔ Q∧P
8. (∨単位) false∨P ⇔ P
9. (∨交換) P∨Q ⇔ P∨Q

「'⇔'の定義に'⇔'を使っている」は、定義用のメタ記号（例えば':≡'）を導入すれば回避できる。ただし、演繹定理があるので、ここらへんはあまり気にしなくてよい。

集合に対する定義と定理

使いそうなものだけ。

1. (集合⊆) A⊆B :⇔ (x∈A ⇒ x∈B)
2. (集合=) A = B :⇔ (A⊆B ∧ B⊆A)
3. (集合∩) x∈A∩B :⇔ (x∈A ∧ x∈B)
4. (集合∪) x∈A∪B :⇔ (x∈A ∨ x∈B)
5. (集合-) x∈A-B :⇔ (x∈A ∧ ¬(x∈B))
6. (∩と⊆) A∩B⊆A, 　A∩B⊆B
7. (∪と⊆) A⊆A∪B, 　B⊆A∪B
8. (∩は単調) A⊆B ⇒ A∩C⊆B∩C
9. (∪は単調) A⊆B ⇒ A∪C⊆B∪C
10. (∩はベキ等) A∩A = A
11. (∪はベキ等) A∪A = A
12. (∩は可換) A∩B = B∩A
13. (∪は可換) A∪B = B∪A

補題

B-(B-A) = A∩B

target // 目標
 B-(B-A) = A∩B
proof // ここから証明開始
 equivalence // ここから同値性の証明
  // 各行が同値な命題、行頭の'⇔'は省略、'by'で根拠を示す
  x∈B-(B-A)
  x∈B ∧ ¬(x∈B-A) by (集合-)
  x∈B ∧ ¬(x∈B ∧ ¬(x∈A)) by (集合-)
  x∈B ∧ (¬(x∈B) ∨ (x∈A)) by (ド・モルガン), (二重否定)
  (x∈B ∧ ¬(x∈B)) ∨ (x∈B ∧ x∈A) by (分配)
  false ∨ (x∈B ∧ x∈A) by (矛盾)
  x∈B ∧ x∈A by (∨単位)
  x∈B∩A by (集合∩)
 end equivalence // 同値性の証明 終わり
 thus x∈B-(B-A) ⇔ x∈B∩A // 'thus'は「念のために言うならば」
 B-(B-A) = B∩A by (集合=)
end proof // 証明終わり
thus B-(B-A) = B∩A

これより

• (補題1) B-(B-A) = A∩B

A = A∩B ⇔ A⊆B

target // 最終的な目標
 A = A∩B ⇔ A⊆B
proof
 target // 入れ子は補助的な目標
   A = A∩B ⇒ A⊆B
 proof
  assume A = A∩B ---(1) // これは仮定
  by the way // 一旦話題を変えるけど
  A∩B ⊆ B by (∩と⊆) // いつだって成立している命題
  A ⊆ B by (1)
  use assumption (1) // 仮定を使う、自然演繹の含意導入
  A = A∩B ⇒ A ⊆ B
 end proof
 thus A = A∩B ⇒ A⊆B ---(2)

 target
   A⊆B ⇒ A = A∩B
 proof
   assume A⊆B ---(3)
   A∩A ⊆ B∩A by (∩は単調)
   A ⊆ B∩A by (∩はベキ等)
   A ⊆ A∩B by (∩は可換)
   use assumptin (3)
   A⊆B ⇒ A ⊆ A∩B
 end proof
 thus A⊆B ⇒ A ⊆ A∩B ---(4)

 A = A∩B ⇔ A⊆B by (2), (4), (⇔定義)
end proof
thus A = A∩B ⇔ A⊆B

これより

• (補題2) A = A∩B ⇔ A⊆B

定理

target
 A = B-(B-A) ⇔ A⊆B
proof
 assume A = B-(B-A) ---(1)
 A = A∩B by (補題1: B-(B-A) = A∩B)
 A⊆B by (補題2: A = A∩B ⇔ A⊆B)
 use assumption (1)
 A = B-(B-A) ⇒ A⊆B ---(2)

 assume A⊆B ---(3)
 by the way
 A∩B ⊆ A by (∩と⊆) ---(4)
 B-(B-A) ⊆ A by (補題1: B-(B-A) = A∩B)
 use assumption (3)
 A⊆B ⇒ B-(B-A) ⊆ A ---(5)

 A = B-(B-A) ⇔ A⊆B by (2), (5), (⇔定義)
end proof
thus A = B-(B-A) ⇔ A⊆B