THEOREM 1

*********

For every set x, there exists an empty subset of x.

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 x is a set

1 Set(x)

Premise

Apply Subset Axiom

2 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & ~a=a]]

Subset, 1

3 Set(null) & ALL(a):[a e null <=> a e x & ~a=a]

E Spec, 2

Define: null

4 Set(null)

Split, 3

5 ALL(a):[a e null <=> a e x & ~a=a]

Split, 3

Prove: null is a subset of x

Suppose...

6 y e null

Premise

Apply definition of null

7 y e null <=> y e x & ~y=y

U Spec, 5

8 [y e null => y e x & ~y=y] & [y e x & ~y=y => y e null]

Iff-And, 7

9 y e null => y e x & ~y=y

Split, 8

10 y e x & ~y=y => y e null

Split, 8

11 y e x & ~y=y

Detach, 9, 6

12 y e x

Split, 11

null is a subset of x

As Required:

13 ALL(b):[b e null => b e x]

4 Conclusion, 6

Prove: ~EXIST(b):b e null

Suppose to the contrary...

14 y e null

Premise

Apply definition of null

15 y e null <=> y e x & ~y=y

U Spec, 5

16 [y e null => y e x & ~y=y] & [y e x & ~y=y => y e null]

Iff-And, 15

17 y e null => y e x & ~y=y

Split, 16

18 y e x & ~y=y => y e null

Split, 16

19 y e x & ~y=y

Detach, 17, 14

20 y e x

Split, 19

21 ~y=y

Split, 19

22 y=y

Reflex

Obtain the contradiction...

23 y=y & ~y=y

Join, 22, 21

As Required:

24 ~EXIST(b):b e null

4 Conclusion, 14

25 ~~ALL(b):~b e null

Quant, 24

As Required:

26 ALL(b):~b e null

Rem DNeg, 25

Joining results...

27 Set(null) & ALL(b):[b e null => b e x]

Join, 4, 13

28 Set(null) & ALL(b):[b e null => b e x]

& ALL(b):~b e null

Join, 27, 26

As Required:

29 ALL(a):[Set(a)

=> EXIST(null):[Set(null) & ALL(b):[b e null => b e a]

& ALL(b):~b e null]]

4 Conclusion, 1