 The following theorem states that pointfree endo-relations induced by bi-

nary endo-relations are essentially the same as these binary endo-relations them-
selves. Thus pointfree binary endo-relations are a generalization of binary endo-
relations.

Theorem 1.

Having specified up to isomorphism (of systems of pointfree re-

lations) the system of pointfree relations induced by binary relations, we can
restore the endo-relation to which corresponds a given pointfree endo-relation
up to isomorphism (of binary relations).

Proof.

Fix a set

A

.

Let

µ

Rel

(

A, A

) be a binary relation (which we are going to restore up to

isomorphism from the corresponding pointfree relation).

We will consider possible domains and possible images

D

=

P

A

.

Let

A

0

be the set of atoms of

D

, that is one-element sets.

Take (using axiom of choice) an arbitrary bijection

f

:

A

0

A

. (Note that

it can be done using only the system of pointfree relations induced by the binary
relations up to isomorphism.)

Let

y

0

, y

1

A

0

be atoms. Take elements

p, q

Rel

(

A

0

, A

0

) such that im

p

=

y

0

, dom

q

=

y

1

(they exist because our system of pointfree relations is induced

by binary relations).

Define binary relation

µ

0

Rel

(

A

0

, A

0

) as:

y

0

µ

0

y

1

iff

q

f

1

µ

f

p

6

=

(for all

y

0

, y

1

A

0

).

Thus we have restored relation

µ

0

from the corresponding pointfree relation.

µ

0

was defined using only properties of orders and the precategory. Thus it is

invariant under isomorphism (of systems of pointfree relations).

Let’s prove that

µ

0

=

f

1

µ

f

(and thus

µ

0

is isomorphic to

µ

). Really,

y

0

µ

0

y

1

q

f

1

µ

f

p

6

=

⊥ ⇔

x

im

p, y

dom

q

: (

x, y

)

f

1

µ

f

(im

p

×

dom

q

)

f

1

µ

f

6

=

∅ ⇔

y

0

(

f

1

µ

f

)

y

1

.

If we take another isomorphism

f

2

f

, then the induced binary

relation

µ

0

2

=

f

1

2

µ

f

2

=

f

1

2

f

µ

0

f

1

f

2

= (

f

1

2

f

)

µ

0

(

f

1

2

f

)

1

.

Thus

µ

0

2

is isomorphic to

µ

0

(and therefore isomorphic to

µ

), because the com-

position

f

1

2

f

is a bijection. We have determined

µ

0

up to isomorphism of

binary relations.

If

µ

2

is a binary relation isomorphic to

µ

0

, then

µ

2

is isomorphic to

µ

and

thus

µ

2

=

f

1

µ

f

for some bijection

f

, so obviously

µ

2

induces the same

(up to isomorphism) pointfree binary relation as

µ

. So we have determined

the sought-for class of pairwise isomorphic binary relations which induce (up
to isomorphism) the same pointfree binary relation as induced by

µ

as these

binary endo-relations which are isomorphic to

µ

0

.

3