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 );
set xx = the Element of L;
set cL = the carrier of L;
Class ((EqRel R), the Element of L) in Class (EqRel R) by EQREL_1:def 3;
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 object such that
A8: y in the carrier of L and
A9: x = Class ((EqRel R),y) by EQREL_1:def 3;
reconsider y = y as Element of L by A8;
reconsider ky = k . y as Element of rngk by A6, FUNCT_1:def 3;
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 8;
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:23;
then [a,b] in R by A3, EQREL_1:19;
then [:k,k:] . (a,b) in id the carrier of L by A2, FUNCT_1:def 7;
then [(k . a),(k . b)] in id the carrier of L by A6, FUNCT_3:def 8;
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 8, ZFMISC_1:def 2;
then [a,b] in EqRel R by A2, A3, A11, FUNCT_1:def 7;
then a in Class ((EqRel R),b) by EQREL_1:19;
hence Class ((EqRel R),a) = Class ((EqRel R),b) by EQREL_1:23; :: 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 3;
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 object such that
A15: a in the carrier of L and
A16: x = Class ((EqRel R),a) by EQREL_1:def 3;
reconsider a = a as Element of L by A15;
take a ; :: thesis:
thus x = Class ((EqRel R),a) by A16; :: thesis:

end;

now :: thesis:

let x1, x2 be object ; :: 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:19;
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 :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng f ; :: thesis:
then consider x being object such that
A25: x in dom f and
A26: y = f . x by FUNCT_1:def 3;
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 3; :: thesis:

end;

assume y in rngk ; :: thesis:
then consider x being object such that
A28: x in dom k and
A29: y = k . x by FUNCT_1:def 3;
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 3;
hence y in rng f by A24, A29, FUNCT_1:def 3; :: 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 object such that
A31: a in the carrier of L and
A32: x = Class ((EqRel R),a) by EQREL_1:def 3;

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:60; :: 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 object such that
A36: b in the carrier of L and
A37: y = Class ((EqRel R),b) by EQREL_1:def 3;
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:59;
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 ;
then Image k,LR are_isomorphic by WAYBEL_1:6;
then reconsider LR = LR as non empty strict Poset by Th15, Th16, Th17;
Image k is complete by WAYBEL_1:54;
then reconsider LR = LR as non empty strict complete Poset by A40, Th18, WAYBEL_1:6;
reconsider LR = LR as strict complete LATTICE ;
Image k is continuous LATTICE by A1, WAYBEL15:14;
then reconsider LR = LR as strict complete continuous LATTICE by A40, WAYBEL15:9, WAYBEL_1:6;
reconsider f9 = f " as Function of (Image k),LR by A23, A30, FUNCT_2:25;
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:56;
take LR ; :: thesis:
thus the carrier of LR = Class (EqRel R) by A4; :: thesis:

now :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume A43: z in the InternalRel of LR ; :: thesis:
then consider a, b being object 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 5;
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 3;
reconsider a = Class ((EqRel R),x) as Element of LR by A4, EQREL_1:def 3;
a <= b by A5, A47;
hence z in the InternalRel of LR by A46, ORDERS_2:def 5; :: 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 :: thesis:

let x be object ; :: 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 3;
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:13
.= f9 . (k . x) by WAYBEL_1:30
.= Class ((EqRel R),x9) by A24, A23, A50, FUNCT_1:32
.= g . x by A48 ;
:: thesis:

end;

then A51: g = f9 * (corestr k) by FUNCT_2:12;
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:11;
g is infs-preserving by A51, A42, Th25;
hence g is CLHomomorphism of L,LR by A53, WAYBEL16:def 1; :: thesis: