let L be complete continuous LATTICE; :: thesis:
let R be Subset of [:L,L:]; :: thesis:
let k be kernel Function of L,L; :: thesis:
assume that
A1: k is directed-sups-preserving and
A2: R = [:k,k:] " (id the carrier of L) ; :: thesis:
A3: R is Equivalence_Relation of the carrier of L by A2, Th2;
set ER = EqRel R;
A4: EqRel R = R by A3, Def1;
set cL = the carrier of L;
A5: dom k = the carrier of L by FUNCT_2:def 1;
then A6: dom [:k,k:] = [:the carrier of L,the carrier of L:] by FUNCT_3:def 9;
consider xx being Element of L;
Class (EqRel R),xx in Class (EqRel R) by EQREL_1:def 5;
then reconsider CER = Class (EqRel R) as non empty Subset-Family of the carrier of L ;
defpred S₁[ set , set ] means ex x, y being Element of L st
( $1 = Class (EqRel R),x & $2 = Class (EqRel R),y & k . x <= k . y );
consider LR being non empty strict RelStr such that
A7: the carrier of LR = CER and
A8: for a, b being Element of LR holds
( a <= b iff S₁[a,b] ) from YELLOW_0:sch 1();
A9: for a, b being Element of the carrier of L holds
( Class (EqRel R),a = Class (EqRel R),b iff k . a = k . b )

proof

let a, b be Element of the carrier of L; :: thesis:

hereby :: thesis:

assume Class (EqRel R),a = Class (EqRel R),b ; :: thesis:
then a in Class (EqRel R),b by EQREL_1:31;
then [a,b] in R by A4, EQREL_1:27;
then [:k,k:] . a,b in id the carrier of L by A2, FUNCT_1:def 13;
then [(k . a),(k . b)] in id the carrier of L by A5, FUNCT_3:def 9;
hence k . a = k . b by RELAT_1:def 10; :: thesis:

end;

A10: [a,b] in [:the carrier of L,the carrier of L:] by ZFMISC_1:def 2;
assume k . a = k . b ; :: thesis:
then [(k . a),(k . b)] in id the carrier of L by RELAT_1:def 10;
then [:k,k:] . a,b in id the carrier of L by A5, FUNCT_3:def 9;
then [a,b] in EqRel R by A2, A4, A6, A10, FUNCT_1:def 13;
then a in Class (EqRel R),b by EQREL_1:27;
hence Class (EqRel R),a = Class (EqRel R),b by EQREL_1:31; :: thesis:

end;

reconsider rngk = rng k as non empty set ;
defpred S₂[ set , set ] means ex a being Element of the carrier of L st
( $1 = Class (EqRel R),a & $2 = k . a );
A11: for x being Element of CER ex y being Element of rngk st S₂[x,y]

proof

let x be Element of CER; :: thesis:
consider y being set such that
A12: ( y in the carrier of L & x = Class (EqRel R),y ) by EQREL_1:def 5;
reconsider y = y as Element of L by A12;
reconsider ky = k . y as Element of rngk by A5, FUNCT_1:def 5;
take ky ; :: thesis:
thus S₂[x,ky] by A12; :: thesis:

end;

consider f being Function of CER,rngk such that
A13: for x being Element of CER holds S₂[x,f . x] from FUNCT_2:sch 3(A11);
A14: dom f = CER by FUNCT_2:def 1;
A15: for x being Element of L holds f . (Class (EqRel R),x) = k . x

proof

let x be Element of L; :: thesis:
reconsider CERx = Class (EqRel R),x as Element of CER by EQREL_1:def 5;
consider a being Element of the carrier of L such that
A16: ( CERx = Class (EqRel R),a & f . CERx = k . a ) by A13;
thus f . (Class (EqRel R),x) = k . x by A9, A16; :: thesis:

end;

set tIR = the InternalRel of LR;
set IR = { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } ;
A17: for x being Element of LR ex a being Element of L st x = Class (EqRel R),a

proof

let x be Element of LR; :: thesis:
x in CER by A7;
then consider a being set such that
A18: ( a in the carrier of L & x = Class (EqRel R),a ) by EQREL_1:def 5;
reconsider a = a as Element of L by A18;
take a ; :: thesis:
thus x = Class (EqRel R),a by A18; :: thesis:

end;

now

let x1, x2 be set ; :: thesis:
assume A19: ( x1 in CER & x2 in CER & f . x1 = f . x2 ) ; :: thesis:
then reconsider x1' = x1 as Element of LR by A7;
reconsider x2' = x2 as Element of LR by A7, A19;
consider a being Element of L such that
A20: x1' = Class (EqRel R),a by A17;
consider b being Element of L such that
A21: x2' = Class (EqRel R),b by A17;
( f . x1' = k . a & f . x2' = k . b ) by A15, A20, A21;
hence x1 = x2 by A9, A19, A20, A21; :: thesis:

end;

then A22: f is one-to-one by FUNCT_2:25;
A23: the carrier of (Image k) = rngk by YELLOW_0:def 15;
then reconsider f = f as Function of LR,(Image k) by A7;

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being set such that
A24: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of LR by A24;
consider a being Element of L such that
A25: x = Class (EqRel R),a by A17;
f . x = k . a by A15, A25;
hence y in rngk by A5, A24, FUNCT_1:def 5; :: thesis:

end;

assume y in rngk ; :: thesis:
then consider x being set such that
A26: ( x in dom k & y = k . x ) by FUNCT_1:def 5;
reconsider x = x as Element of L by A26;
A27: Class (EqRel R),x in CER by EQREL_1:def 5;
f . (Class (EqRel R),x) = k . x by A15;
hence y in rng f by A14, A26, A27, FUNCT_1:def 5; :: thesis:

end;

then A28: rng f = rngk by TARSKI:2;
for x, y being Element of LR holds
( x <= y iff f . x <= f . y )

proof

let x, y be Element of LR; :: thesis:
x in CER by A7;
then consider a being set such that
A29: ( a in the carrier of L & x = Class (EqRel R),a ) by EQREL_1:def 5;
reconsider a = a as Element of L by A29;
y in CER by A7;
then consider b being set such that
A30: ( b in the carrier of L & y = Class (EqRel R),b ) by EQREL_1:def 5;
reconsider b = b as Element of L by A30;
A31: ( f . x = k . a & f . y = k . b ) by A15, A29, A30;

hereby :: thesis:

assume x <= y ; :: thesis:
then consider c, d being Element of L such that
A32: ( x = Class (EqRel R),c & y = Class (EqRel R),d & k . c <= k . d ) by A8;
( f . x = k . c & f . y = k . d ) by A15, A32;
hence f . x <= f . y by A32, YELLOW_0:61; :: thesis:

end;

assume f . x <= f . y ; :: thesis:
then k . a <= k . b by A31, YELLOW_0:60;
hence x <= y by A8, A29, A30; :: thesis:

end;

then A33: f is isomorphic by A22, A23, A28, WAYBEL_0:66;
then A34: LR, Image k are_isomorphic by WAYBEL_1:def 8;
then A35: Image k,LR are_isomorphic by WAYBEL_1:7;
A36: Image k is continuous LATTICE by A1, WAYBEL15:16;
reconsider LR = LR as non empty strict Poset by A35, Th15, Th16, Th17;
Image k is complete by WAYBEL_1:57;
then reconsider LR = LR as non empty strict complete Poset by A34, Th18, WAYBEL_1:7;
reconsider LR = LR as strict complete LATTICE ;
reconsider LR = LR as strict complete continuous LATTICE by A34, A36, WAYBEL15:11, WAYBEL_1:7;
take LR ; :: thesis:
thus the carrier of LR = Class (EqRel R) by A7; :: thesis:

now

let z be set ; :: thesis:

hereby :: thesis:

assume A37: z in the InternalRel of LR ; :: thesis:
then consider a, b being set such that
A38: ( a in CER & b in CER & z = [a,b] ) by A7, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of LR by A7, A38;
a <= b by A37, A38, ORDERS_2:def 9;
then consider x, y being Element of L such that
A39: ( a = Class (EqRel R),x & b = Class (EqRel R),y & k . x <= k . y ) by A8;
thus z in { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } by A38, A39; :: thesis:

end;

assume z in { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } ; :: thesis:
then consider x, y being Element of L such that
A40: ( z = [(Class (EqRel R),x),(Class (EqRel R),y)] & k . x <= k . y ) ;
reconsider a = Class (EqRel R),x as Element of LR by A7, EQREL_1:def 5;
reconsider b = Class (EqRel R),y as Element of LR by A7, EQREL_1:def 5;
a <= b by A8, A40;
hence z in the InternalRel of LR by A40, ORDERS_2:def 9; :: thesis:

end;

hence the InternalRel of LR = { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } by TARSKI:2; :: thesis:
let g be Function of L,LR; :: thesis:
assume A41: for x being Element of L holds g . x = Class (EqRel R),x ; :: thesis:
reconsider f' = f " as Function of (Image k),LR by A22, A23, A28, FUNCT_2:31;
A42: f' is isomorphic by A33, WAYBEL_0:68;

now

let x be set ; :: thesis:
assume A43: x in the carrier of L ; :: thesis:
then reconsider x' = x as Element of L ;
A44: dom (corestr k) = the carrier of L by FUNCT_2:def 1;
A45: f . (Class (EqRel R),x') = k . x' by A15;
A46: Class (EqRel R),x' in CER by EQREL_1:def 5;
thus (f' * (corestr k)) . x = f' . ((corestr k) . x) by A43, A44, FUNCT_1:23
.= f' . (k . x) by WAYBEL_1:32
.= Class (EqRel R),x' by A14, A22, A45, A46, FUNCT_1:54
.= g . x by A41 ; :: thesis:

end;

then A47: g = f' * (corestr k) by FUNCT_2:18;
A48: corestr k is infs-preserving by WAYBEL_1:59;
A49: corestr k is directed-sups-preserving by A1, Th22;
A50: f' is infs-preserving by A42, WAYBEL13:20;
reconsider f' = f' as sups-preserving Function of (Image k),LR by A42, WAYBEL13:20;
A51: f' is directed-sups-preserving ;
A52: g is infs-preserving by A47, A48, A50, Th26;
g is directed-sups-preserving by A47, A49, A51, WAYBEL15:13;
hence g is CLHomomorphism of L,LR by A52, WAYBEL16:def 1; :: thesis: