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, Th37;
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 Th38;
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 set such that
A4:
u in the carrier of L
and
A5:
x = Class (EqRel R),u
by A2, EQREL_1:def 5;
y in the carrier of LR
;
then consider v being set such that
A6:
v in the carrier of L
and
A7:
y = Class (EqRel R),v
by A2, EQREL_1:def 5;
hereby ( "/\" x,L <= "/\" y,L implies x <= y )
assume
x <= y
;
"/\" x,L <= "/\" y,Lthen
[x,y] in the
InternalRel of
LR
by ORDERS_2:def 9;
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, ZFMISC_1:33;
(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 9; verum