set k = kernel_op R;
( kernel_op R is directed-sups-preserving & R = [:(kernel_op R),(kernel_op R):] " (id the carrier of L) )
by B1, Th36;
then consider LR being strict complete continuous LATTICE such that
A1:
the carrier of LR = Class (EqRel R)
and
A2:
the InternalRel of LR = { [(Class ((EqRel R),x)),(Class ((EqRel R),y))] where x, y is Element of L : (kernel_op R) . x <= (kernel_op R) . y }
and
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
by Th37;
take
LR
; ( the carrier of LR = Class (EqRel R) & ( for x, y being Element of LR holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) ) ) )
thus
the carrier of LR = Class (EqRel R)
by A1; for x, y being Element of LR holds
( x <= y iff "/\" (x,L) <= "/\" (y,L) )
let x, y be Element of LR; ( x <= y iff "/\" (x,L) <= "/\" (y,L) )
x in the carrier of LR
;
then consider u being set such that
A3:
u in the carrier of L
and
A4:
x = Class ((EqRel R),u)
by A1, EQREL_1:def 3;
y in the carrier of LR
;
then consider v being set such that
A5:
v in the carrier of L
and
A6:
y = Class ((EqRel R),v)
by A1, EQREL_1:def 3;
hereby ( "/\" (x,L) <= "/\" (y,L) implies x <= y )
assume
x <= y
;
"/\" (x,L) <= "/\" (y,L)then
[x,y] in the
InternalRel of
LR
by ORDERS_2:def 5;
then consider u9,
v9 being
Element of
L such that A7:
[x,y] = [(Class ((EqRel R),u9)),(Class ((EqRel R),v9))]
and A8:
(kernel_op R) . u9 <= (kernel_op R) . v9
by A2;
A9:
(
x = Class (
(EqRel R),
u9) &
y = Class (
(EqRel R),
v9) )
by A7, XTUPLE_0:1;
(kernel_op R) . u9 = inf (Class ((EqRel R),u9))
by B1, Def3;
hence
"/\" (
x,
L)
<= "/\" (
y,
L)
by B1, A8, A9, Def3;
verum
end;
assume A10:
"/\" (x,L) <= "/\" (y,L)
; x <= y
reconsider u = u, v = v as Element of L by A3, A5;
( (kernel_op R) . u = inf (Class ((EqRel R),u)) & (kernel_op R) . v = inf (Class ((EqRel R),v)) )
by B1, Def3;
then
[x,y] in the InternalRel of LR
by A2, A4, A6, A10;
hence
x <= y
by ORDERS_2:def 5; verum