THEOREM 2

*********

All empty sets are equal.

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com

PROOF

*****

Suppose null and null' are empty sets

1 Set(null) & ALL(a):~a e null

& Set(null') & ALL(a):~a e null'

Premise

2 Set(null)

Split, 1

3 ALL(a):~a e null

Split, 1

4 Set(null')

Split, 1

5 ALL(a):~a e null'

Split, 1

Apply Axiom of Set Equality

6 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]

Set Equality

7 ALL(b):[Set(null) & Set(b) => [null=b <=> ALL(c):[c e null <=> c e b]]]

U Spec, 6

8 Set(null) & Set(null') => [null=null' <=> ALL(c):[c e null <=> c e null']]

U Spec, 7

9 Set(null) & Set(null')

Join, 2, 4

10 null=null' <=> ALL(c):[c e null <=> c e null']

Detach, 8, 9

11 [null=null' => ALL(c):[c e null <=> c e null']]

& [ALL(c):[c e null <=> c e null'] => null=null']

Iff-And, 10

12 null=null' => ALL(c):[c e null <=> c e null']

Split, 11

Sufficient: For null = null'

13 ALL(c):[c e null <=> c e null'] => null=null'

Split, 11

'=>'

Prove: ALL(c):[c e null => c e null']

Suppose...

14 x e null

Premise

15 ~x e null

U Spec, 3

16 ~x e null => x e null'

Arb Cons, 14

17 x e null'

Detach, 16, 15

As Required:

18 ALL(c):[c e null => c e null']

4 Conclusion, 14

'<='

Prove: ALL(c):[c e null' => c e null]

Suppose...

19 x e null'

Premise

20 ~x e null'

U Spec, 5

21 ~x e null' => x e null

Arb Cons, 19

22 x e null

Detach, 21, 20

As Required:

23 ALL(c):[c e null' => c e null]

4 Conclusion, 19

Joining results...

24 ALL(c):[[c e null => c e null'] & [c e null' => c e null]]

Join, 18, 23

25 ALL(c):[c e null <=> c e null']

Iff-And, 24

26 null=null'

Detach, 13, 25

As Required:

27 ALL(null):ALL(null'):[Set(null) & ALL(a):~a e null

& Set(null') & ALL(a):~a e null'

=> null=null']

4 Conclusion, 1