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 A1, Th36;
then consider LR being strict complete continuous LATTICE such that
A2:
the carrier of LR = Class (EqRel R)
and
A3:
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 A2; 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 object such that
A4:
u in the carrier of L
and
A5:
x = Class ((EqRel R),u)
by A2, EQREL_1:def 3;
y in the carrier of LR
;
then consider v being object such that
A6:
v in the carrier of L
and
A7:
y = Class ((EqRel R),v)
by A2, 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 A8:
[x,y] = [(Class ((EqRel R),u9)),(Class ((EqRel R),v9))]
and A9:
(kernel_op R) . u9 <= (kernel_op R) . v9
by A3;
A10:
(
x = Class (
(EqRel R),
u9) &
y = Class (
(EqRel R),
v9) )
by A8, XTUPLE_0:1;
(kernel_op R) . u9 = inf (Class ((EqRel R),u9))
by A1, Def3;
hence
"/\" (
x,
L)
<= "/\" (
y,
L)
by A1, A9, A10, Def3;
verum
end;
assume A11:
"/\" (x,L) <= "/\" (y,L)
; x <= y
reconsider u = u, v = v as Element of L by A4, A6;
( (kernel_op R) . u = inf (Class ((EqRel R),u)) & (kernel_op R) . v = inf (Class ((EqRel R),v)) )
by A1, Def3;
then
[x,y] in the InternalRel of LR
by A3, A5, A7, A11;
hence
x <= y
by ORDERS_2:def 5; verum