 Theorem 75

S

B

.

Proof

Let

x

S

. Then

Ex

R

;

M

(

Ex

) =

E

1

Ex

=

x

;

x

im

M

=

B

.

Obvious 24

E

is a bijection from

S

to

R

.

Theorem 76

M

is a bijection from

B

to

B

.

Proof

Surjectivity of

M

is obvious. Let’s prove injectivity. Let

a, b

B

and

M

(

a

) =

M

(

b

). Consider all cases:

a, b

R M

(

a

) =

E

1

a

;

M

(

b

) =

E

1

b

;

E

1

a

=

E

1

b

; thus

a

=

b

because

E

1

is a bijection.

a

R

,

b

6∈

R M

(

a

) =

E

1

a

;

M

(

b

) = (

t

;

b

);

M

(

a

)

S

;

M

(

b

)

6∈

S

. Thus

M

(

a

)

6

=

M

(

b

).

a

6∈

R

,

b

R

Analogous,

a, b

6∈

R M

(

a

) = (

t

;

a

);

M

(

b

) = (

t

;

b

). Thus

M

(

a

) =

M

(

b

) implies

a

=

b

.

Theorem 77

M

E

= id

S

.

Proof

Let

x

S

. Then

Ex

R

;

M

(

Ex

) =

E

1

Ex

=

x

.

Obvious 25

E

=

M

1

|

S

.

References

 Roland Backhouse.

Galois Connections and Fixed Point Calculus

. 2001.

 Grzegorz Bancerek. Prime ideals and filters.

Formalized Mathematics

, 8(2),

1996.

 Garrett Birkhoff. Neutral elements in general lattices.

Bulletin of the

American Mathematical Society

, 46(8):702–705, 1940.

 Francis Borceux and Maria-Cristina Pediccio. On primeness and maximal-

ity of filters.

Cahiers de Topologie et G´eom´etrie Diff´erentielle Cat´egoriques

,

30(2):167–181, 1989.

 M. Erne, J. Koslowski, A. Melton, and G. E. Strecker.

A primer on Galois

connections

.

 J´an Jakub´ık. Center of infinitely distributive lattices.

Matem. fyz. casopis

,

8:116–120, 1957.

60