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 : (kernel_op R) . x <= (kernel_op R) . y }
and
for g being Function of L,LR st ( for x being Element of 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 holds
( x <= y iff "/\" x,L <= "/\" y,L ) ) )
thus
the carrier of LR = Class (EqRel R)
by A2; for x, y being Element of holds
( x <= y iff "/\" x,L <= "/\" y,L )
let x, y be Element of ; ( 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 u',
v' being
Element of
such that A8:
[x,y] = [(Class (EqRel R),u'),(Class (EqRel R),v')]
and A9:
(kernel_op R) . u' <= (kernel_op R) . v'
by A3;
A10:
(
x = Class (EqRel R),
u' &
y = Class (EqRel R),
v' )
by A8, ZFMISC_1:33;
(kernel_op R) . u' = inf (Class (EqRel R),u')
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 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