 I will denote

F

¡(

A

;

B

) =

f

(

A

;

B

;

F

)

j

F

2

F

¡[

A

;

B

]

g

.

Remark 12.

It should be instead be denoted as

(

F

¡)(

A

;

B

)

but for brevity I omit

.

4 Before the diagram

Next we will prove the below theorem

35

(the theorem with a diagram). First we will present

parts of this theorem as several lemmas, and then then state a statement about the diagram which
concisely summarizes the lemmas (and their easy consequences).

Obvious 13.

up

¡(

Src

f

;

Dst

f

)

f

= (

up

f

)

\

¡

for every reloid

f

.

Conjecture 14.

F

(

B

)

up

A

X

is not a lter for some lter

X 2

F

¡(

A

;

B

)

for some sets

A

,

B

.

Remark 15.

About this conjecture see also:

http://goo.gl/DHyuuU

http://goo.gl/4a6wY6

Lemma 16.

Let

A

,

B

be sets. The following are mutually inverse order isomorphisms between

F

¡(

A

;

B

)

and

FCD

(

A

;

B

)

:

1.

A 7!

d

FCD

up

A

;

2.

f

7!

up

¡(

A

;

B

)

f

.

Proof.

Let's prove that up

¡(

A

;

B

)

f

is a lter for every funcoid

f

. We need to prove that

P

\

Q

2

up

f

whenever

P

=

\

i

=0

;:::;n

¡

1

(

X

i

Y

i

[

X

i

B

)

and

Q

=

\

j

=0

;:::;m

¡

1

(

X

j

0

Y

j

0

[

X

j

0

B

)

:

This follows from

P

2

up

f

, 8

i

2

0

; :::; n

¡

1:

h

f

i

X

i

Y

i

and likewise for

Q

, so having

h

f

i

(

X

i

\

X

j

0

)

Y

i

\

Y

j

0

for every

i

= 0

; :::; n

¡

1

and

j

= 0

; :::; m

¡

1

. From this it follows

((

X

i

\

X

j

0

)

(

Y

i

\

Y

j

0

))

[

(

X

i

\

X

j

0

B

)

f

and thus

P

\

Q

2

up

f

.

Let

A

,

B

be lters on

¡

. Let

d

FCD

up

A

=

d

FCD

up

B

. We need to prove

A

=

B

. (The rest

follows from proof of the theorem 6.104 from my book [

1

]). We have:

[TODO: Separate the rst

equality below from theorem 6.104 into a separate lemma.]

A

=

l

FCD

f

X

Y

[

X

B

2 A j

X

2

P

A; Y

2

P

B

g

=

l

FCD

f

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

9

P

2 A

:

P

X

Y

[

X

B

g

=

l

FCD

f

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

9

P

2 A

:

h

P

i

X

Y

g

=

(*)

l

FCD

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

l

fh

P

i

X

j

A

2

up

Ag v

Y

=

l

FCD

8

<

:

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

l

(

h

P

i

X

j

A

2

up

l

RLD

up

A

)

v

Y

9

=

;

=

l

FCD

8

<

:

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

*

(

FCD

)

l

RLD

up

A

+

X

v

Y

9

=

;

=

(**)

l

FCD

8

<

:

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

*

l

FCD

up

l

RLD

up

A

+

X

v

Y

9

=

;

=

l

FCD

8

<

:

X

Y

[

X

B

j

X

2

P

A; Y

2

P

B ;

*

l

FCD

up

A

+

X

v

Y

9

=

;

:

Before the diagram

3