 Proof.

(

Src

f

;

Z

0

)

is a finitely meet-closed filtrator by theorem 29 in  and with separable core

by theorem 37 and corollary 10 in ; thus we can apply theorem 25.

h

f

i

T

Src

f

S

⊆ h

f

i

X

for every

X

S

and thus

h

f

i

T

Src

f

S

T

Dst

f

hh

f

ii

S

.

Taking into account properties of generalized filter bases:

h

f

i

\

Src

f

S

=

\

Dst

f

hh

f

ii

up

\

S

=

\

Dst

f

{hh

f

ii

X

| ∃P ∈

S

:

X

up

P }

=

\

Dst

f

{h

f

i

X

| ∃P ∈

S

:

X

up

P } ⊇

\

Dst

f

{h

f

iP | P ∈

S

}

=

\

Dst

f

hh

f

ii

S.

3.4 The preorder of pointfree funcoids

The

preorder of pointfree funcoids

is defined by the formula

f

g

[

f

]

[

g

]

for every pointfree

funcoids

f

and

g

.

Remark 28.

It is enough to define preorder of pointfree funcoids on every set

FCD

(

A

;

B

)

where

A

and

B

are posets. We do not need to compare pointfree funcoids with different sources or

destinations.

Theorem 29.

If

A

and

B

are separable posets then

FCD

(

A

;

B

)

is a poset.

Proof.

From the theorem 12.

Theorem 30.

Let

(

A

;

Z

0

)

and

(

B

;

Z

1

)

are primary filtrators over boolean lattices. Then for

R

P

FCD

(

A

;

B

)

and

X

Z

0

,

Y

Z

1

we have:

1.

X

S

FCD

(

A

;

B

)

R

Y

⇔ ∃

f

R

:

X

[

f

]

Y

;

2.

S

FCD

(

A

;

B

)

R

X

=

S

B

{h

f

i

X

|

f

R

}

.

Proof.

2.

αX

=

def

S

B

{h

f

i

X

|

f

R

}

(by corollary 8 in  all joins on

B

exist). We have

α

0

A

= 0

B

;

α

(

I

Z

0

J

) =

[

B

{h

f

i

(

I

Z

0

J

)

|

f

R

}

=

[

B

{h

f

i

(

I

A

J

)

|

f

R

}

=

[

B

{h

f

i

I

B

h

f

i

J

|

f

R

}

=

[

B

{h

f

i

I

|

f

R

} ∪

B

[

B

{h

f

i

J

|

f

R

}

=

αI

B

α J

(used the theorem 15). By the theorem 26 the function

α

can be continued to

h

h

i

for a

h

FCD

(

A

;

B

)

. Obviously

f

R

:

h

f .

(4)

And

h

is the least element of

FCD

(

A

;

B

)

for which holds the condition (4). So

h

=

S

FCD

(

A

;

B

)

R

.

1.

X

[

S

FCD

R

]

Y

Y

B

h

S

FCD

R

i

X

0

B

Y

B

S

B

{h

f

i

X

|

f

R

}

0

B

⇔ ∃

f

R

:

Y

B

h

f

i

X

0

B

⇔ ∃

f

R

:

X

[

f

]

Y

(used the theorem 40 in ).

Corollary 31.

If

(

A

;

Z

0

)

and

(

B

;

Z

1

)

are primary filtrators over boolean lattices then

FCD

(

A

;

B

)

is a complete lattice.

6

Section 3