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:
set ER = EqRel R;
R is Equivalence_Relation of the carrier of L by A2, Th2;
then A3: EqRel R = R by Def1;
reconsider rngk = rng k as non empty set ;
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 xx being Element of L;
set cL = the carrier 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 ;
consider LR being non empty strict RelStr such that
A4: the carrier of LR = CER and
A5: for a, b being Element of LR holds
( a <= b iff S₁[a,b] ) from YELLOW_0:sch 1();
defpred S₂[ set , set ] means ex a being Element of the carrier of L st
( $1 = Class (EqRel R),a & $2 = k . a );
A6: dom k = the carrier of L by FUNCT_2:def 1;
A7: 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
A8: y in the carrier of L and
A9: x = Class (EqRel R),y by EQREL_1:def 5;
reconsider y = y as Element of L by A8;
reconsider ky = k . y as Element of rngk by A6, FUNCT_1:def 5;
take ky ; :: thesis:
thus S₂[x,ky] by A9; :: thesis:

end;

consider f being Function of CER,rngk such that
A10: for x being Element of CER holds S₂[x,f . x] from FUNCT_2:sch 3(A7);
A11: dom [:k,k:] = [:the carrier of L,the carrier of L:] by A6, FUNCT_3:def 9;
A12: 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 A3, 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 A6, FUNCT_3:def 9;
hence k . a = k . b by RELAT_1:def 10; :: thesis:

end;

assume k . a = k . b ; :: thesis:
then [(k . a),(k . b)] in id the carrier of L by RELAT_1:def 10;
then ( [a,b] in [:the carrier of L,the carrier of L:] & [:k,k:] . a,b in id the carrier of L ) by A6, FUNCT_3:def 9, ZFMISC_1:def 2;
then [a,b] in EqRel R by A2, A3, A11, 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;

A13: 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;
ex a being Element of the carrier of L st
( CERx = Class (EqRel R),a & f . CERx = k . a ) by A10;
hence f . (Class (EqRel R),x) = k . x by A12; :: thesis:

end;

A14: 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 A4;
then consider a being set such that
A15: a in the carrier of L and
A16: x = Class (EqRel R),a by EQREL_1:def 5;
reconsider a = a as Element of L by A15;
take a ; :: thesis:
thus x = Class (EqRel R),a by A16; :: thesis:

end;

now

let x1, x2 be set ; :: thesis:
assume that
A17: x1 in CER and
A18: x2 in CER and
A19: f . x1 = f . x2 ; :: thesis:
reconsider x19 = x1 as Element of LR by A4, A17;
consider a being Element of L such that
A20: x19 = Class (EqRel R),a by A14;
reconsider x29 = x2 as Element of LR by A4, A18;
consider b being Element of L such that
A21: x29 = Class (EqRel R),b by A14;
A22: f . x29 = k . b by A13, A21;
f . x19 = k . a by A13, A20;
hence x1 = x2 by A12, A19, A20, A21, A22; :: thesis:

end;

then A23: f is one-to-one by FUNCT_2:25;
set tIR = the InternalRel of LR;
A24: dom f = CER by FUNCT_2:def 1;
reconsider f = f as Function of LR,(Image k) by A4, YELLOW_0:def 15;

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being set such that
A25: x in dom f and
A26: y = f . x by FUNCT_1:def 5;
reconsider x = x as Element of LR by A25;
consider a being Element of L such that
A27: x = Class (EqRel R),a by A14;
f . x = k . a by A13, A27;
hence y in rngk by A6, A26, FUNCT_1:def 5; :: thesis:

end;

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

end;

then A30: ( the carrier of (Image k) = rngk & rng f = rngk ) by TARSKI:2, YELLOW_0:def 15;
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 A4;
then consider a being set such that
A31: a in the carrier of L and
A32: x = Class (EqRel R),a by EQREL_1:def 5;

hereby :: thesis:

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

end;

reconsider a = a as Element of L by A31;
assume A35: f . x <= f . y ; :: thesis:
y in CER by A4;
then consider b being set such that
A36: b in the carrier of L and
A37: y = Class (EqRel R),b by EQREL_1:def 5;
reconsider b = b as Element of L by A36;
A38: f . y = k . b by A13, A37;
f . x = k . a by A13, A32;
then k . a <= k . b by A38, A35, YELLOW_0:60;
hence x <= y by A5, A32, A37; :: thesis:

end;

then A39: f is isomorphic by A23, A30, WAYBEL_0:66;
then A40: LR, Image k are_isomorphic by WAYBEL_1:def 8;
then Image k,LR are_isomorphic by WAYBEL_1:7;
then reconsider LR = LR as non empty strict Poset by Th15, Th16, Th17;
Image k is complete by WAYBEL_1:57;
then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:7;
reconsider LR = LR as strict complete LATTICE ;
Image k is continuous LATTICE by A1, WAYBEL15:16;
then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:11, WAYBEL_1:7;
reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:31;
set IR = { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } ;
A41: f9 is isomorphic by A39, WAYBEL_0:68;
then A42: ( corestr k is infs-preserving & f9 is infs-preserving ) by WAYBEL13:20, WAYBEL_1:59;
take LR ; :: thesis:
thus the carrier of LR = Class (EqRel R) by A4; :: thesis:

now

let z be set ; :: thesis:

hereby :: thesis:

assume A43: z in the InternalRel of LR ; :: thesis:
then consider a, b being set such that
A44: ( a in CER & b in CER ) and
A45: z = [a,b] by A4, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of LR by A4, A44;
a <= b by A43, A45, ORDERS_2:def 9;
then ex x, y being Element of L st
( a = Class (EqRel R),x & b = Class (EqRel R),y & k . x <= k . y ) by A5;
hence z in { [(Class (EqRel R),x),(Class (EqRel R),y)] where x, y is Element of L : k . x <= k . y } by A45; :: 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
A46: z = [(Class (EqRel R),x),(Class (EqRel R),y)] and
A47: k . x <= k . y ;
reconsider b = Class (EqRel R),y as Element of LR by A4, EQREL_1:def 5;
reconsider a = Class (EqRel R),x as Element of LR by A4, EQREL_1:def 5;
a <= b by A5, A47;
hence z in the InternalRel of LR by A46, 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 A48: for x being Element of L holds g . x = Class (EqRel R),x ; :: thesis:

now

let x be set ; :: thesis:
assume A49: x in the carrier of L ; :: thesis:
then reconsider x9 = x as Element of L ;
A50: ( f . (Class (EqRel R),x9) = k . x9 & Class (EqRel R),x9 in CER ) by A13, EQREL_1:def 5;
dom (corestr k) = the carrier of L by FUNCT_2:def 1;
hence (f9 * (corestr k)) . x = f9 . ((corestr k) . x) by A49, FUNCT_1:23
.= f9 . (k . x) by WAYBEL_1:32
.= Class (EqRel R),x9 by A24, A23, A50, FUNCT_1:54
.= g . x by A48 ;
:: thesis:

end;

then A51: g = f9 * (corestr k) by FUNCT_2:18;
A52: corestr k is directed-sups-preserving by A1, Th22;
reconsider f9 = f9 as sups-preserving Function of (Image k),LR by A41, WAYBEL13:20;
f9 is directed-sups-preserving ;
then A53: g is directed-sups-preserving by A51, A52, WAYBEL15:13;
g is infs-preserving by A51, A42, Th26;
hence g is CLHomomorphism of L,LR by A53, WAYBEL16:def 1; :: thesis: