let L be lower-bounded LATTICE; :: thesis:
set A = the carrier of L;
set D = BasicDF L;
set S = the ExtensionSeq of the carrier of L, BasicDF L;
set FS = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A1: ( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A2: the ExtensionSeq of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)] by Def20;
the carrier of L c= union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } by A1, A2, ZFMISC_1:74;
then reconsider FS = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } as non empty set ;
reconsider FD = union { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } as distance_function of FS,L by Th41;
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 Def8;
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 Def8;
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 Def8;
A10: field e2 = FS by ORDERS_1:12;

let x, y be object ; :: 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:15;
FD . (x9,y9) <= b by A7, A12;
then FD . (x9,y9) <= b "\/" a by A11, ORDERS_2:3;
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:12;
for u, v being object st [u,v] in e3 holds
[u,v] in e1 "\/" e2

proof

let u, v be object ; :: 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:15;
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 Th42;
A21: u in FS by A14, A16, RELAT_1:15;
defpred S₁[ set , object ] 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 object st S₁[m,w]

proof

let m be Nat; :: thesis:
assume m in Seg 5 ; :: thesis:
then not not m = 1 & ... & not m = 5 by Lm3;

per cases ;

suppose A23: m = 1 ; :: thesis:

take x ; :: thesis:
thus S₁[m,x] by A23; :: thesis:

end;

suppose A24: m = 2 ; :: thesis:

take z1 ; :: thesis:
thus S₁[m,z1] by A24; :: thesis:

end;

suppose A25: m = 3 ; :: thesis:

take z2 ; :: thesis:
thus S₁[m,z2] by A25; :: thesis:

end;

suppose A26: m = 4 ; :: thesis:

take z3 ; :: thesis:
thus S₁[m,z3] by A26; :: thesis:

end;

suppose A27: m = 5 ; :: thesis:

take y ; :: thesis:
thus S₁[m,y] by A27; :: 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
A28: dom h = Seg 5 and
A29: 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 ) ) ;
A30: len h = 5 by A28, FINSEQ_1:def 3;
A31: 5 in Seg 5 ;
A32: 4 in Seg 5 ;
A33: 1 in Seg 5 ;
then A34: u = h . 1 by A29;
A35: 2 in Seg 5 ;
A36: for j being Nat st 1 <= j & j < len h holds
[(h . j),(h . (j + 1))] in e1 \/ e2

proof

let j be Nat; :: thesis:
assume ( 1 <= j & j < len h ) ; :: thesis:
then not not j = 1 & ... & not j = 4 by A30, Lm2;

per cases ;

suppose A37: j = 1 ; :: thesis:

[x,z1] in e1 by A9, A17;
then [(h . 1),z1] in e1 by A29, A33;
then [(h . 1),(h . 2)] in e1 by A29, A35;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A37, XBOOLE_0:def 3; :: thesis:

end;

suppose A38: j = 3 ; :: thesis:

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

end;

suppose A39: j = 2 ; :: thesis:

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

end;

suppose A40: j = 4 ; :: thesis:

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

end;

v = h . 5 by A29, A31
.= h . (len h) by A28, FINSEQ_1:def 3 ;
hence [u,v] in e1 "\/" e2 by A21, A30, A34, A36, EQREL_1:28; :: thesis:

end;

then A41: e3 c= e1 "\/" e2 by RELAT_1:def 3;
A42: field e1 = FS by ORDERS_1:12;

now :: thesis:

let x, y be object ; :: thesis:
A43: a <= a "\/" b by YELLOW_0:22;
assume A44: [x,y] in e1 ; :: thesis:
then reconsider x9 = x, y9 = y as Element of FS by A42, RELAT_1:15;
FD . (x9,y9) <= a by A9, A44;
then FD . (x9,y9) <= a "\/" b by A43, ORDERS_2:3;
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 A45: e1 "\/" e2 c= e3 by EQREL_1:def 2;
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:60
.= ((alpha FD) . a) "\/" ((alpha FD) . b) by YELLOW_0:41
.= e1 "\/" e2 by A8, A6, Th10
.= (alpha FD) . (a "\/" b) by A4, A45, A41
.= (alpha FD) . (sup {a,b}) by YELLOW_0:41 ;
hence alpha FD preserves_sup_of {a,b} by A3; :: thesis:

end;

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

proof

A49: { 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;

end;

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

proof

let w be object ; :: thesis:
A72: ( the ExtensionSeq of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A73: ( the ExtensionSeq of the carrier of L, BasicDF L . 0) `2 in { (( the ExtensionSeq of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } ;
A74: the ExtensionSeq of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)] by Def20;
A75: BasicDF L c= FD by A73, A74, ZFMISC_1:74;
assume w in the carrier of L ; :: thesis:
then consider z being object such that
A76: z in [: the carrier of L, the carrier of L:] and
A77: (BasicDF L) . z = w by A71, FUNCT_2:11;
take z ; :: thesis:
the carrier of L c= FS by A72, A74, ZFMISC_1:74;
then [: the carrier of L, the carrier of L:] c= [:FS,FS:] by ZFMISC_1:96;
hence z in [:FS,FS:] by A76; :: thesis:
z in dom (BasicDF L) by A76, FUNCT_2:def 1;
hence w = FD . z by A77, A75, GRFUNC_1:2; :: thesis:

end;

then rng FD = the carrier of L by FUNCT_2:10;
then FD is onto by FUNCT_2:def 3;
hence f is one-to-one by Th15; :: thesis:
for e1, e2 being Equivalence_Relation of FS
for x, y being object 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 Th43;
hence type_of (Image f) <= 3 by A48, Th13; :: thesis: