theorem Th37:
for
L being
complete continuous LATTICE for
R being
Subset of
[:L,L:] for
k being
kernel Function of
L,
L st
k is
directed-sups-preserving &
R = [:k,k:] " (id the carrier of L) holds
ex
LR being
strict complete continuous LATTICE st
( the
carrier of
LR = Class (EqRel R) & the
InternalRel of
LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : k . x <= k . y } & ( for
g being
Function of
L,
LR st ( for
x being
Element of
L holds
g . x = Class (
(EqRel R),
x) ) holds
g is
CLHomomorphism of
L,
LR ) )