let L be lower-bounded LATTICE; :: thesis:
set A = the carrier of L;
set D = BasicDF L;
consider S being ExtensionSeq of the carrier of L, BasicDF L;
set FS = union { ((S . i) `1 ) where i is Element of NAT : verum } ;
A1: (S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
A2: S . 0 = [the carrier of L,(BasicDF L)] by Def21;
then (S . 0 ) `1 = the carrier of L by MCART_1:def 1;
then the carrier of L c= union { ((S . i) `1 ) where i is Element of NAT : verum } by A1, ZFMISC_1:92;
then reconsider FS = union { ((S . i) `1 ) where i is Element of NAT : verum } as non empty set ;
reconsider FD = union { ((S . i) `2 ) where i is Element of NAT : verum } as distance_function of FS,L by Th44;
alpha FD is join-preserving

set f = alpha FD;
let a, b be Element of L; :: according to WAYBEL_0:def 35 :: thesis:
A3: ex_sup_of (alpha FD) .: {a,b}, EqRelLATT FS by YELLOW_0:17;
consider e3 being Equivalence_Relation of FS such that
A4: e3 = (alpha FD) . (a "\/" b) and
A5: for x, y being Element of FS holds
( [x,y] in e3 iff FD . x,y <= a "\/" b ) by Def9;
consider e2 being Equivalence_Relation of FS such that
A6: e2 = (alpha FD) . b and
A7: for x, y being Element of FS holds
( [x,y] in e2 iff FD . x,y <= b ) by Def9;
consider e1 being Equivalence_Relation of FS such that
A8: e1 = (alpha FD) . a and
A9: for x, y being Element of FS holds
( [x,y] in e1 iff FD . x,y <= a ) by Def9;
A10: field e2 = FS by ORDERS_1:97;

let x, y be set ; :: thesis:
A11: b <= b "\/" a by YELLOW_0:22;
assume A12: [x,y] in e2 ; :: thesis:
then reconsider x9 = x, y9 = y as Element of FS by A10, RELAT_1:30;
FD . x9,y9 <= b by A7, A12;
then FD . x9,y9 <= b "\/" a by A11, ORDERS_2:26;
hence [x,y] in e3 by A5; :: thesis:

end;

then A13: e2 c= e3 by RELAT_1:def 3;
A14: field e3 = FS by ORDERS_1:97;
for u, v being set st [u,v] in e3 holds
[u,v] in e1 "\/" e2

proof

let u, v be set ; :: thesis:
A15: 3 in Seg 5 ;
assume A16: [u,v] in e3 ; :: thesis:
then reconsider x = u, y = v as Element of FS by A14, RELAT_1:30;
FD . x,y <= a "\/" b by A5, A16;
then consider z1, z2, z3 being Element of FS such that
A17: FD . x,z1 = a and
A18: FD . z2,z3 = a and
A19: FD . z1,z2 = b and
A20: FD . z3,y = b by Th45;
A21: u in FS by A14, A16, RELAT_1:30;
defpred S₁[ set , set ] means ( ( $1 = 1 implies $2 = x ) & ( $1 = 2 implies $2 = z1 ) & ( $1 = 3 implies $2 = z2 ) & ( $1 = 4 implies $2 = z3 ) & ( $1 = 5 implies $2 = y ) );
A22: for m being Nat st m in Seg 5 holds
ex w being set st S₁[m,w]

proof

let m be Nat; :: thesis:
assume A23: m in Seg 5 ; :: thesis:

per cases by A23, Lm3;

suppose A24: m = 1 ; :: thesis:

take w = x; :: thesis:
thus S₁[m,w] by A24; :: thesis:

end;

suppose A25: m = 2 ; :: thesis:

take w = z1; :: thesis:
thus S₁[m,w] by A25; :: thesis:

end;

suppose A26: m = 3 ; :: thesis:

take w = z2; :: thesis:
thus S₁[m,w] by A26; :: thesis:

end;

suppose A27: m = 4 ; :: thesis:

take w = z3; :: thesis:
thus S₁[m,w] by A27; :: thesis:

end;

suppose A28: m = 5 ; :: thesis:

take w = y; :: thesis:
thus S₁[m,w] by A28; :: thesis:

end;

ex p being FinSequence st
( dom p = Seg 5 & ( for k being Nat st k in Seg 5 holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A22);
then consider h being FinSequence such that
A29: dom h = Seg 5 and
A30: for m being Nat st m in Seg 5 holds
( ( m = 1 implies h . m = x ) & ( m = 2 implies h . m = z1 ) & ( m = 3 implies h . m = z2 ) & ( m = 4 implies h . m = z3 ) & ( m = 5 implies h . m = y ) ) ;
A31: len h = 5 by A29, FINSEQ_1:def 3;
A32: 5 in Seg 5 ;
A33: 4 in Seg 5 ;
A34: 1 in Seg 5 ;
then A35: u = h . 1 by A30;
A36: 2 in Seg 5 ;
A37: for j being Element of NAT st 1 <= j & j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2

proof

let j be Element of NAT ; :: thesis:
assume A38: ( 1 <= j & j < len h ) ; :: thesis:

per cases by A31, A38, Lm2;

suppose A39: j = 1 ; :: thesis:

[x,z1] in e1 by A9, A17;
then [(h . 1),z1] in e1 by A30, A34;
then [(h . 1),(h . 2)] in e1 by A30, A36;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A39, XBOOLE_0:def 3; :: thesis:

end;

suppose A40: j = 3 ; :: thesis:

[z2,z3] in e1 by A9, A18;
then [(h . 3),z3] in e1 by A30, A15;
then [(h . 3),(h . 4)] in e1 by A30, A33;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A40, XBOOLE_0:def 3; :: thesis:

end;

suppose A41: j = 2 ; :: thesis:

[z1,z2] in e2 by A7, A19;
then [(h . 2),z2] in e2 by A30, A36;
then [(h . 2),(h . 3)] in e2 by A30, A15;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A41, XBOOLE_0:def 3; :: thesis:

end;

suppose A42: j = 4 ; :: thesis:

[z3,y] in e2 by A7, A20;
then [(h . 4),y] in e2 by A30, A33;
then [(h . 4),(h . 5)] in e2 by A30, A32;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A42, XBOOLE_0:def 3; :: thesis:

end;

v = h . 5 by A30, A32
.= h . (len h) by A29, FINSEQ_1:def 3 ;
hence [u,v] in e1 "\/" e2 by A21, A31, A35, A37, EQREL_1:36; :: thesis:

end;

then A43: e3 c= e1 "\/" e2 by RELAT_1:def 3;
A44: field e1 = FS by ORDERS_1:97;

now

let x, y be set ; :: thesis:
A45: a <= a "\/" b by YELLOW_0:22;
assume A46: [x,y] in e1 ; :: thesis:
then reconsider x9 = x, y9 = y as Element of FS by A44, RELAT_1:30;
FD . x9,y9 <= a by A9, A46;
then FD . x9,y9 <= a "\/" b by A45, ORDERS_2:26;
hence [x,y] in e3 by A5; :: thesis:

end;

then e1 c= e3 by RELAT_1:def 3;
then e1 \/ e2 c= e3 by A13, XBOOLE_1:8;
then A47: e1 "\/" e2 c= e3 by EQREL_1:def 3;
dom (alpha FD) = the carrier of L by FUNCT_2:def 1;
then sup ((alpha FD) .: {a,b}) = sup {((alpha FD) . a),((alpha FD) . b)} by FUNCT_1:118
.= ((alpha FD) . a) "\/" ((alpha FD) . b) by YELLOW_0:41
.= e1 "\/" e2 by A8, A6, Th10
.= (alpha FD) . (a "\/" b) by A4, A47, A43, XBOOLE_0:def 10
.= (alpha FD) . (sup {a,b}) by YELLOW_0:41 ;
hence alpha FD preserves_sup_of {a,b} by A3, WAYBEL_0:def 31; :: thesis:

end;

then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by Th16;
A48: dom f = the carrier of L by FUNCT_2:def 1;
A49: Image f = subrelstr (rng f) by YELLOW_2:def 2;
A50: ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )

proof

A51: {the carrier of L} <> {{the carrier of L}}

proof

assume {the carrier of L} = {{the carrier of L}} ; :: thesis:
then {the carrier of L} in {the carrier of L} by TARSKI:def 1;
hence contradiction ; :: thesis:

end;

consider A9 being non empty set , d9 being distance_function of A9,L, Aq9 being non empty set , dq9 being distance_function of Aq9,L such that
A52: Aq9,dq9 is_extension_of A9,d9 and
A53: S . 0 = [A9,d9] and
A54: S . (0 + 1) = [Aq9,dq9] by Def21;
( A9 = the carrier of L & d9 = BasicDF L ) by A2, A53, ZFMISC_1:33;
then consider q being QuadrSeq of BasicDF L such that
A55: Aq9 = NextSet (BasicDF L) and
A56: dq9 = NextDelta q by A52, Def20;
ConsecutiveSet the carrier of L,{} = the carrier of L by Th24;
then reconsider Q = Quadr q,{} as Element of [:the carrier of L,the carrier of L,the carrier of L,the carrier of L:] ;
A57: (S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum } ;
succ {} c= DistEsti (BasicDF L) by Lm4;
then {} in DistEsti (BasicDF L) by ORDINAL1:33;
then A58: {} in dom q by Th28;
then q . {} in rng q by FUNCT_1:def 5;
then q . {} in { [u,v,a9,b9] where u, v is Element of the carrier of L, a9, b9 is Element of L : (BasicDF L) . u,v <= a9 "\/" b9 } by Def14;
then consider u, v being Element of the carrier of L, a, b being Element of L such that
A59: q . {} = [u,v,a,b] and
(BasicDF L) . u,v <= a "\/" b ;
consider e being Equivalence_Relation of FS such that
A60: e = f . b and
A61: for x, y being Element of FS holds
( [x,y] in e iff FD . x,y <= b ) by Def9;
A62: Quadr q,{} = [u,v,a,b] by A58, A59, Def15;
(S . 1) `2 = NextDelta q by A54, A56, MCART_1:def 2;
then A63: NextDelta q c= FD by A57, ZFMISC_1:92;
A64: {{the carrier of L}} in {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}} by ENUMSET1:def 1;
then A65: {{the carrier of L}} in the carrier of L \/ {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}} by XBOOLE_0:def 3;
take e ; :: thesis:
e in rng f by A48, A60, FUNCT_1:def 5;
hence e in the carrier of (Image f) by A49, YELLOW_0:def 15; :: thesis:
A66: (S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
(S . 1) `1 = NextSet (BasicDF L) by A54, A55, MCART_1:def 1;
then A67: NextSet (BasicDF L) c= FS by A66, ZFMISC_1:92;
new_set the carrier of L = new_set (ConsecutiveSet the carrier of L,{} ) by Th24
.= ConsecutiveSet the carrier of L,(succ {} ) by Th25 ;
then new_set the carrier of L c= NextSet (BasicDF L) by Lm4, Th32;
then A68: new_set the carrier of L c= FS by A67, XBOOLE_1:1;
A69: {{the carrier of L}} in new_set the carrier of L by A64, XBOOLE_0:def 3;
A70: {the carrier of L} in {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}} by ENUMSET1:def 1;
then {the carrier of L} in the carrier of L \/ {{the carrier of L},{{the carrier of L}},{{{the carrier of L}}}} by XBOOLE_0:def 3;
then reconsider W = {the carrier of L}, V = {{the carrier of L}} as Element of FS by A68, A69;
A71: ( ConsecutiveSet the carrier of L,{} = the carrier of L & ConsecutiveDelta q,{} = BasicDF L ) by Th24, Th29;
ConsecutiveDelta q,(succ {} ) = new_bi_fun (BiFun (ConsecutiveDelta q,{} ),(ConsecutiveSet the carrier of L,{} ),L),(Quadr q,{} ) by Th30
.= new_bi_fun (BasicDF L),Q by A71, Def16 ;
then new_bi_fun (BasicDF L),Q c= NextDelta q by Lm4, Th35;
then A72: new_bi_fun (BasicDF L),Q c= FD by A63, XBOOLE_1:1;
( dom (new_bi_fun (BasicDF L),Q) = [:(new_set the carrier of L),(new_set the carrier of L):] & {the carrier of L} in new_set the carrier of L ) by A70, FUNCT_2:def 1, XBOOLE_0:def 3;
then [{the carrier of L},{{the carrier of L}}] in dom (new_bi_fun (BasicDF L),Q) by A65, ZFMISC_1:106;
then FD . W,V = (new_bi_fun (BasicDF L),Q) . {the carrier of L},{{the carrier of L}} by A72, GRFUNC_1:8
.= Q `4 by Def11
.= b by A62, MCART_1:def 11 ;
then [{the carrier of L},{{the carrier of L}}] in e by A61;
hence e <> id FS by A51, RELAT_1:def 10; :: thesis:

end;

take FS ; :: thesis:
take f ; :: thesis:
BasicDF L is onto by Th43;
then A73: rng (BasicDF L) = the carrier of L by FUNCT_2:def 3;
for w being set st w in the carrier of L holds
ex z being set st
( z in [:FS,FS:] & w = FD . z )

proof

let w be set ; :: thesis:
A74: (S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
A75: (S . 0 ) `2 in { ((S . i) `2 ) where i is Element of NAT : verum } ;
A76: S . 0 = [the carrier of L,(BasicDF L)] by Def21;
then BasicDF L = (S . 0 ) `2 by MCART_1:def 2;
then A77: BasicDF L c= FD by A75, ZFMISC_1:92;
assume w in the carrier of L ; :: thesis:
then consider z being set such that
A78: z in [:the carrier of L,the carrier of L:] and
A79: (BasicDF L) . z = w by A73, FUNCT_2:17;
take z ; :: thesis:
the carrier of L = (S . 0 ) `1 by A76, MCART_1:def 1;
then the carrier of L c= FS by A74, ZFMISC_1:92;
then [:the carrier of L,the carrier of L:] c= [:FS,FS:] by ZFMISC_1:119;
hence z in [:FS,FS:] by A78; :: thesis:
z in dom (BasicDF L) by A78, FUNCT_2:def 1;
hence w = FD . z by A79, A77, GRFUNC_1:8; :: thesis:

end;

then rng FD = the carrier of L by FUNCT_2:16;
then FD is onto by FUNCT_2:def 3;
hence f is one-to-one by Th17; :: thesis:
for e1, e2 being Equivalence_Relation of FS
for x, y being set st e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 3 + 2 & x,y are_joint_by F,e1,e2 ) by Th46;
hence type_of (Image f) <= 3 by A50, Th15; :: thesis: