THEOREM 3

*********

Every empty set can be expressed as a family of sets of which there exists a union.

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...

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

Premise

2 Set(null)

Split, 1

3 ALL(a):~a e null

Split, 1

4 x e null

Premise

Apply definition of null

5 ~x e null

U Spec, 3

6 ~x e null => Set(x)

Arb Cons, 4

7 Set(x)

Detach, 6, 5

As Required:

8 ALL(a):[a e null => Set(a)]

4 Conclusion, 4

Apply Axiom of Arbitrary Union

9 ALL(f):[Set(f) & ALL(a):[a e f => Set(a)]

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

Arb Union

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

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

U Spec, 9

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

Join, 2, 8

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

Detach, 10, 11

13 Set(unull) & ALL(b):[b e unull <=> EXIST(c):[c e null & b e c]]

E Spec, 12

As Required:

14 EXIST(unull):[Set(unull) & ALL(b):[b e unull <=> EXIST(c):[c e null & b e c]]]

E Gen, 13

Joining results...

15 ALL(a):[a e null => Set(a)]

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

Join, 8, 14

As Required:

16 ALL(null):[Set(null) & ALL(a):~a e null

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

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

4 Conclusion, 1