 6 Rest

Lemma 24.

Every non-empty set has a well ordering with greatest element.

Proof.

Take an arbitrary well ordering of our set and move the rst element to the end of the

order.

Theorem 25.

L

2

[

f

]

)

[

f

]

\

Q

i

2

dom

A

atoms

L

i

=

/

;

for every pre-multifuncoid

f

of the form whose

elements are atomic posets.

Proof.

If arity

f

= 0

our theorem is trivial, so let arity

f

=

/ 0

. Let

v

is a well-ordering of arity

f

with greatest element

m

(it exists by the lemma).

Let

is a function which maps non-least elements of posets into atoms under these elements and

least elements into themselves. (Note that

is dened on least elements only for completeness,

is never taken on a least element in the proof below.)

[TODO: Fix the universal set paradox here.]

Dene a transnite sequence

a

by transnite induction with the formula

a

c

h

f

i

c

(

a

j

X

(

c

)

nf

c

g

[

L

j

(

arity

f

)

n

X

(

c

)

)

:

Let

b

c

=

a

j

X

(

c

)

nf

c

g

[

L

j

(

arity

f

)

n

X

(

c

)

. Then

a

c

h

f

i

c

b

c

.

Let us prove by transnite induction

a

c

2

atoms

L

c

:

a

c

h

f

i

c

L

j

(

arity

f

)

nf

c

g

vh

f

i

c

L

j

(

arity

f

)

nf

c

g

. Thus

a

c

v

L

c

.

[TODO: Is it true for

pre

-multifun-

coids?]

The only thing remained to prove is that

h

f

i

c

b

c

=

/ 0

that is

h

f

i

c

(

a

j

X

(

c

)

nf

c

g

[

L

j

(

arity

f

)

n

X

(

c

)

) =

/ 0

that is

y

/

h

f

i

c

b

c

??

L

c

/

h

f

i

c

b

c

,

b

c

(0)

/

h

f

i

0

(

b

c

j

(

arity

f

)

nf

0

g

[f

c

;

L

c

g

)

,

a

0

/

h

f

i

0

(

a

j

X

(

c

)

nf

0

;c

g

[

L

j

(

arity

f

)

n

X

(

c

)

[f

c

;

L

c

g

)

,

a

0

/

h

f

i

0

(

a

j

X

(

c

)

nf

0

;c

g

[

L

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

(

a

0

/

h

f

i

0

(

a

j

X

(

c

)

nf

0

;c

g

[

a

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

,

a

0

/

h

f

i

0

(

a

j

(

X

(

c

)

nf

0

;c

g

)

[

((

arity

f

)

n

X

(

c

))

[f

c

g

)

,

a

0

/

h

f

i

0

(

a

j

(

arity

f

)

nf

0

g

)

,

h

f

i

0

(

L

j

(

arity

f

)

nf

0

g

)

/

h

f

i

0

(

a

j

(

arity

f

)

nf

0

g

)

.

??

a

0

h

f

i

0

(

L

j

(

arity

f

)

nf

0

g

)

??
??Two ways to prove:??

L

c

/

h

f

i

c

b

c

,

b

c

(

k

)

/

h

f

i

k

(

b

c

j

(

arity

f

)

nf

k

g

[f

c

;

L

c

g

)

,

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

k;c

g

[

L

j

(

arity

f

)

n

X

(

c

)

[f

c

;

L

c

g

)

,

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

k;c

g

[

L

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

(

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

k;c

g

[

a

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

,

a

k

/

h

f

i

k

(

a

j

(

X

(

c

)

nf

k;c

g

)

[

((

arity

f

)

n

X

(

c

))

[f

c

g

)

,

a

k

/

h

f

i

k

(

a

j

(

arity

f

)

nf

k

g

)

??

L

c

/

h

f

i

c

b

c

,

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

c;k

g

[

L

j

(

arity

f

)

n

X

(

c

)

[f

(

c

;

L

c

)

g

)

,

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

c;k

g

[

L

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

(

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

c;k

g

[

a

j

((

arity

f

)

n

X

(

c

))

[f

c

g

)

,

a

k

/

h

f

i

k

(

a

j

(

arity

f

)

nf

k

g

)

??

y

/

h

f

i

c

b

c

,

a

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

c;k

g

[

L

j

(

arity

f

)

n

X

(

c

)

[f

(

c

;

y

)

g

)

(

a

k

/

h

f

i

k

(

a

j

X

(

k

)

nf

k

g

[

L

j

(

arity

f

)

n

X

(

c

)

[f

(

c

;

y

)

g

)

y

/

h

f

i

c

b

c

,

L

k

/

h

f

i

k

(

a

j

X

(

c

)

nf

c

g

[

L

j

(

arity

f

)

n

(

X

(

c

)

[f

k

g

)

[f

(

c

;

y

)

g

)

(

??

a

m

h

f

i

m

(

i

2

(

arity

f

)

n f

m

g

:

a

i

) =

h

f

i

m

a

j

(

arity

f

)

nf

m

g

;

a

m

h

f

i

m

a

j

(

arity

f

)

nf

m

g

;

a

m

/

h

f

i

m

a

j

(

arity

f

)

nf

m

g

;

a

2

[

f

]

.

Theorem 26.

Let

A

=

A

i

2

n

is a family of boolean lattices.

A relation

2

P

Q

atoms

F

(

A

i

)

such that for every

a

2

Q

atoms

F

(

A

i

)

8

A

2

a

:

\

Y

i

2

n

atoms

"

A

i

A

i

=

/

; )

a

2

(3)

can be continued till the function

f

for a unique staroid

f

of the form

i

2

n

:

P

(

A

i

)

. The funcoid

f

is completary.

8

Section 6