let L be lower-bounded modular LATTICE; :: thesis:
set A = the carrier of L;
set D = BasicDF L;
set S = the ExtensionSeq2 of the carrier of L, BasicDF L;
set FS = union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A1: ( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A2: the ExtensionSeq2 of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)] by Def11;
the carrier of L c= union { (( the ExtensionSeq2 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 ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } as non empty set ;
reconsider FD = union { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } as distance_function of FS,L by Th32;
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 e2 being Equivalence_Relation of FS such that
A4: e2 = (alpha FD) . b and
A5: for x, y being Element of FS holds
( [x,y] in e2 iff FD . (x,y) <= b ) by LATTICE5:def 8;
consider e1 being Equivalence_Relation of FS such that
A6: e1 = (alpha FD) . a and
A7: for x, y being Element of FS holds
( [x,y] in e1 iff FD . (x,y) <= a ) by LATTICE5:def 8;
consider e3 being Equivalence_Relation of FS such that
A8: e3 = (alpha FD) . (a "\/" b) and
A9: for x, y being Element of FS holds
( [x,y] in e3 iff FD . (x,y) <= a "\/" b ) by LATTICE5:def 8;
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 A5, A12;
then FD . (x9,y9) <= b "\/" a by A11, ORDERS_2:3;
hence [x,y] in e3 by A9; :: thesis:

end;

then A13: e2 c= e3 ;
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: Seg 4 = { n where n is Nat : ( 1 <= n & n <= 4 ) } by FINSEQ_1:def 1;
then A16: 3 in Seg 4 ;
assume A17: [u,v] in e3 ; :: thesis:
then reconsider x = u, y = v as Element of FS by A14, RELAT_1:15;
A18: FD . (x,y) <= a "\/" b by A9, A17;
then consider z1, z2 being Element of FS such that
A19: FD . (x,z1) = a and
A20: FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b and
A21: FD . (z2,y) = a by Th33;
A22: u in FS by A14, A17, 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 = y ) );
A23: for m being Nat st m in Seg 4 holds
ex w being object st S₁[m,w]

proof

let m be Nat; :: thesis:
assume A24: m in Seg 4 ; :: thesis:

per cases by A24, Lm3;

suppose A25: m = 1 ; :: thesis:

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

end;

suppose A26: m = 2 ; :: thesis:

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

end;

suppose A27: m = 3 ; :: thesis:

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

end;

suppose A28: m = 4 ; :: thesis:

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

end;

ex p being FinSequence st
( dom p = Seg 4 & ( for k being Nat st k in Seg 4 holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A23);
then consider h being FinSequence such that
A29: dom h = Seg 4 and
A30: for m being Nat st m in Seg 4 holds
( ( m = 1 implies h . m = x ) & ( m = 2 implies h . m = z1 ) & ( m = 3 implies h . m = z2 ) & ( m = 4 implies h . m = y ) ) ;
A31: len h = 4 by A29, FINSEQ_1:def 3;
A32: 4 in Seg 4 by A15;
A33: 1 in Seg 4 by A15;
then A34: u = h . 1 by A30;
A35: 2 in Seg 4 by A15;
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 A37: ( 1 <= j & j < len h ) ; :: thesis:

per cases by A31, A37, Lm4;

suppose A38: j = 1 ; :: thesis:

[x,z1] in e1 by A7, A19;
then [(h . 1),z1] in e1 by A30, A33;
then [(h . 1),(h . 2)] in e1 by A30, A35;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A38, XBOOLE_0:def 3; :: thesis:

end;

suppose A39: j = 2 ; :: thesis:

(FD . (x,y)) "\/" a <= (a "\/" b) "\/" a by A18, WAYBEL_1:2;
then (FD . (x,y)) "\/" a <= b "\/" (a "\/" a) by LATTICE3:14;
then (FD . (x,y)) "\/" a <= b "\/" a by YELLOW_5:1;
then ((FD . (x,y)) "\/" a) "/\" b <= b "/\" (b "\/" a) by WAYBEL_1:1;
then ((FD . (x,y)) "\/" a) "/\" b <= b by LATTICE3:18;
then [z1,z2] in e2 by A5, A20;
then [(h . 2),z2] in e2 by A30, A35;
then [(h . 2),(h . 3)] in e2 by A30, A16;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A39, XBOOLE_0:def 3; :: thesis:

end;

suppose A40: j = 3 ; :: thesis:

[z2,y] in e1 by A7, A21;
then [(h . 3),y] in e1 by A30, A16;
then [(h . 3),(h . 4)] in e1 by A30, A32;
hence [(h . j),(h . (j + 1))] in e1 \/ e2 by A40, XBOOLE_0:def 3; :: thesis:

end;

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

end;

then A41: e3 c= e1 "\/" e2 ;
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 A7, A44;
then FD . (x9,y9) <= a "\/" b by A43, ORDERS_2:3;
hence [x,y] in e3 by A9; :: thesis:

end;

then e1 c= e3 ;
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 A6, A4, LATTICE5:10
.= (alpha FD) . (a "\/" b) by A8, 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 LATTICE5:14;
A46: dom f = the carrier of L by FUNCT_2:def 1;
A47: ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )

proof

A48: { 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
A49: Aq9,dq9 is_extension2_of A9,d9 and
A50: the ExtensionSeq2 of the carrier of L, BasicDF L . 0 = [A9,d9] and
A51: the ExtensionSeq2 of the carrier of L, BasicDF L . (0 + 1) = [Aq9,dq9] by Def11;
( A9 = the carrier of L & d9 = BasicDF L ) by A2, A50, XTUPLE_0:1;
then consider q being QuadrSeq of BasicDF L such that
A52: Aq9 = NextSet2 (BasicDF L) and
A53: dq9 = NextDelta2 q by A49;
ConsecutiveSet2 ( the carrier of L,{}) = the carrier of L by Th14;
then reconsider Q = Quadr2 (q,{}) as Element of [: the carrier of L, the carrier of L, the carrier of L, the carrier of L:] ;
A54: ( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `2 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } ;
succ {} c= DistEsti (BasicDF L) by Th1;
then {} in DistEsti (BasicDF L) by ORDINAL1:21;
then A55: {} in dom q by LATTICE5:25;
then q . {} in rng q by FUNCT_1:def 3;
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 LATTICE5:def 13;
then consider u, v being Element of the carrier of L, a, b being Element of L such that
A56: q . {} = [u,v,a,b] and
(BasicDF L) . (u,v) <= a "\/" b ;
consider e being Equivalence_Relation of FS such that
A57: e = f . b and
A58: for x, y being Element of FS holds
( [x,y] in e iff FD . (x,y) <= b ) by LATTICE5:def 8;
Quadr2 (q,{}) = [u,v,a,b] by A55, A56, Def6;
then A59: b = Q `4_4 ;
[Aq9,dq9] `2 = NextDelta2 q by A53;
then A60: NextDelta2 q c= FD by A54, A51, ZFMISC_1:74;
A61: {{ the carrier of L}} in {{ the carrier of L},{{ the carrier of L}}} by TARSKI:def 2;
then A62: {{ the carrier of L}} in 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 A46, A57, FUNCT_1:def 3;
hence e in the carrier of (Image f) by YELLOW_0:def 15; :: thesis:
A63: ( the ExtensionSeq2 of the carrier of L, BasicDF L . 1) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
[Aq9,dq9] `1 = NextSet2 (BasicDF L) by A52;
then A64: NextSet2 (BasicDF L) c= FS by A63, A51, ZFMISC_1:74;
new_set2 the carrier of L = new_set2 (ConsecutiveSet2 ( the carrier of L,{})) by Th14
.= ConsecutiveSet2 ( the carrier of L,(succ {})) by Th15 ;
then new_set2 the carrier of L c= NextSet2 (BasicDF L) by Th1, Th21;
then A65: new_set2 the carrier of L c= FS by A64;
A66: {{ the carrier of L}} in new_set2 the carrier of L by A61, XBOOLE_0:def 3;
A67: { the carrier of L} in {{ the carrier of L},{{ the carrier of L}}} by TARSKI:def 2;
then { the carrier of L} in 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 A65, A66;
A68: ( ConsecutiveSet2 ( the carrier of L,{}) = the carrier of L & ConsecutiveDelta2 (q,{}) = BasicDF L ) by Th14, Th18;
ConsecutiveDelta2 (q,(succ {})) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,{})),(ConsecutiveSet2 ( the carrier of L,{})),L)),(Quadr2 (q,{}))) by Th19
.= new_bi_fun2 ((BasicDF L),Q) by A68, LATTICE5:def 15 ;
then new_bi_fun2 ((BasicDF L),Q) c= NextDelta2 q by Th1, Th24;
then A69: new_bi_fun2 ((BasicDF L),Q) c= FD by A60;
( dom (new_bi_fun2 ((BasicDF L),Q)) = [:(new_set2 the carrier of L),(new_set2 the carrier of L):] & { the carrier of L} in new_set2 the carrier of L ) by A67, FUNCT_2:def 1, XBOOLE_0:def 3;
then [{ the carrier of L},{{ the carrier of L}}] in dom (new_bi_fun2 ((BasicDF L),Q)) by A62, ZFMISC_1:87;
then FD . (W,V) = (new_bi_fun2 ((BasicDF L),Q)) . ({ the carrier of L},{{ the carrier of L}}) by A69, GRFUNC_1:2
.= (((BasicDF L) . ((Q `1_4),(Q `2_4))) "\/" (Q `3_4)) "/\" (Q `4_4) by Def4 ;
then FD . (W,V) <= b by A59, YELLOW_0:23;
then [{ the carrier of L},{{ the carrier of L}}] in e by A58;
hence e <> id FS by A48, RELAT_1:def 10; :: thesis:

end;

A70: now :: thesis:

consider e being Equivalence_Relation of FS such that
e in the carrier of (Image f) and
A71: e <> id FS by A47;
assume FS is trivial ; :: thesis:
then consider x being object such that
A72: FS = {x} by ZFMISC_1:131;
A73: ( [:{x},{x}:] = {[x,x]} & id {x} = {[x,x]} ) by SYSREL:13, ZFMISC_1:29;
field e = {x} by A72, EQREL_1:9;
then id FS c= e by A72, RELAT_2:1;
hence contradiction by A72, A71, A73; :: thesis:

end;

BasicDF L is onto by LATTICE5:40;
then A74: 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:
A75: ( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `1 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `1) where i is Element of NAT : verum } ;
A76: ( the ExtensionSeq2 of the carrier of L, BasicDF L . 0) `2 in { (( the ExtensionSeq2 of the carrier of L, BasicDF L . i) `2) where i is Element of NAT : verum } ;
A77: the ExtensionSeq2 of the carrier of L, BasicDF L . 0 = [ the carrier of L,(BasicDF L)] by Def11;
A78: BasicDF L c= FD by A76, A77, ZFMISC_1:74;
assume w in the carrier of L ; :: thesis:
then consider z being object such that
A79: z in [: the carrier of L, the carrier of L:] and
A80: (BasicDF L) . z = w by A74, FUNCT_2:11;
take z ; :: thesis:
the carrier of L c= FS by A75, A77, 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 A79; :: thesis:
z in dom (BasicDF L) by A79, FUNCT_2:def 1;
hence w = FD . z by A80, A78, GRFUNC_1:2; :: thesis:

end;

then rng FD = the carrier of L by FUNCT_2:10;
then A81: FD is onto by FUNCT_2:def 3;
reconsider FS = FS as non trivial set by A70;
take FS ; :: according to LATTICE8:def 2 :: thesis:
reconsider f = f as Homomorphism of L,(EqRelLATT FS) ;
take f ; :: thesis:
thus f is one-to-one by A81, LATTICE5:15; :: thesis:
reconsider FD = FD as distance_function of FS,L ;
thus Image f is finitely_typed :: thesis:

proof

take FS ; :: according to LATTICE8:def 1 :: thesis:
thus for e being object st e in the carrier of (Image f) holds
e is Equivalence_Relation of FS :: thesis:

proof

let e be object ; :: thesis:
assume e in the carrier of (Image f) ; :: thesis:
then e in rng f by YELLOW_0:def 15;
then consider x being object such that
A82: x in dom f and
A83: e = f . x by FUNCT_1:def 3;
reconsider x = x as Element of L by A82;
ex E being Equivalence_Relation of FS st
( E = f . x & ( for u, v being Element of FS holds
( [u,v] in E iff FD . (u,v) <= x ) ) ) by LATTICE5:def 8;
hence e is Equivalence_Relation of FS by A83; :: thesis:

end;

take 2 + 2 ; :: thesis:
thus 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 = 2 + 2 & x,y are_joint_by F,e1,e2 ) by Th34; :: thesis:

end;

thus ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) :: thesis:

proof

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

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 = 2 + 2 & x,y are_joint_by F,e1,e2 ) by Th34;
hence type_of (Image f) <= 2 by A47, LATTICE5:13; :: thesis: