let L be lower-bounded modular LATTICE; :: thesis: L has_a_representation_of_type<= 2
set A = the carrier of L;
set D = BasicDF L;
consider S being ExtensionSeq2 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 Def12;
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 Th33;
alpha FD is join-preserving
proof
set f = alpha FD;
let a, b be Element of L; :: according to WAYBEL_0:def 35 :: thesis: alpha FD preserves_sup_of {a,b}
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 9;
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 9;
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 9;
A10: field e2 = FS by ORDERS_1:97;
now
let x, y be set ; :: thesis: ( [x,y] in e2 implies [x,y] in e3 )
A11: b <= b "\/" a by YELLOW_0:22;
assume A12: [x,y] in e2 ; :: thesis: [x,y] in e3
then reconsider x9 = x, y9 = y as Element of FS by A10, RELAT_1:30;
FD . x9,y9 <= b by A5, A12;
then FD . x9,y9 <= b "\/" a by A11, ORDERS_2:26;
hence [x,y] in e3 by A9; :: thesis: verum
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: ( [u,v] in e3 implies [u,v] in e1 "\/" e2 )
A15: Seg 4 = { n where n is Element of NAT : ( 1 <= n & n <= 4 ) } by FINSEQ_1:def 1;
then A16: 3 in Seg 4 ;
assume A17: [u,v] in e3 ; :: thesis: [u,v] in e1 "\/" e2
then reconsider x = u, y = v as Element of FS by A14, RELAT_1:30;
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 Th34;
A22: u in FS by A14, A17, RELAT_1:30;
defpred S1[ set , set ] 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 set st S1[m,w]
proof
let m be Nat; :: thesis: ( m in Seg 4 implies ex w being set st S1[m,w] )
assume A24: m in Seg 4 ; :: thesis: ex w being set st S1[m,w]
per cases ( m = 1 or m = 2 or m = 3 or m = 4 ) by A24, Lm3;
suppose A25: m = 1 ; :: thesis: ex w being set st S1[m,w]
take w = x; :: thesis: S1[m,w]
thus S1[m,w] by A25; :: thesis: verum
end;
suppose A26: m = 2 ; :: thesis: ex w being set st S1[m,w]
take w = z1; :: thesis: S1[m,w]
thus S1[m,w] by A26; :: thesis: verum
end;
suppose A27: m = 3 ; :: thesis: ex w being set st S1[m,w]
take w = z2; :: thesis: S1[m,w]
thus S1[m,w] by A27; :: thesis: verum
end;
suppose A28: m = 4 ; :: thesis: ex w being set st S1[m,w]
take w = y; :: thesis: S1[m,w]
thus S1[m,w] by A28; :: thesis: verum
end;
end;
end;
ex p being FinSequence st
( dom p = Seg 4 & ( for k being Nat st k in Seg 4 holds
S1[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 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: ( 1 <= j & j < len h implies [(h . j),(h . (j + 1))] in e1 \/ e2 )
assume A37: ( 1 <= j & j < len h ) ; :: thesis: [(h . j),(h . (j + 1))] in e1 \/ e2
per cases ( j = 1 or j = 2 or j = 3 ) by A31, A37, Lm4;
suppose A38: j = 1 ; :: thesis: [(h . j),(h . (j + 1))] in e1 \/ e2
[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: verum
end;
suppose A39: j = 2 ; :: thesis: [(h . j),(h . (j + 1))] in e1 \/ e2
(FD . x,y) "\/" a <= (a "\/" b) "\/" a by A18, WAYBEL_1:3;
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:2;
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: verum
end;
suppose A40: j = 3 ; :: thesis: [(h . j),(h . (j + 1))] in e1 \/ e2
[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: verum
end;
end;
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:36; :: thesis: verum
end;
then A41: e3 c= e1 "\/" e2 by RELAT_1:def 3;
A42: field e1 = FS by ORDERS_1:97;
now
let x, y be set ; :: thesis: ( [x,y] in e1 implies [x,y] in e3 )
A43: a <= a "\/" b by YELLOW_0:22;
assume A44: [x,y] in e1 ; :: thesis: [x,y] in e3
then reconsider x9 = x, y9 = y as Element of FS by A42, RELAT_1:30;
FD . x9,y9 <= a by A7, A44;
then FD . x9,y9 <= a "\/" b by A43, ORDERS_2:26;
hence [x,y] in e3 by A9; :: thesis: verum
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 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 A6, A4, LATTICE5:10
.= (alpha FD) . (a "\/" b) by A8, A45, A41, 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: verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by LATTICE5:16;
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: contradiction
then {the carrier of L} in {the carrier of L} by TARSKI:def 1;
hence contradiction ; :: thesis: verum
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: S . 0 = [A9,d9] and
A51: S . (0 + 1) = [Aq9,dq9] by Def12;
( A9 = the carrier of L & d9 = BasicDF L ) by A2, A50, ZFMISC_1:33;
then consider q being QuadrSeq of BasicDF L such that
A52: Aq9 = NextSet2 (BasicDF L) and
A53: dq9 = NextDelta2 q by A49, Def11;
ConsecutiveSet2 the carrier of L,{} = the carrier of L by Th15;
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: (S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum } ;
succ {} c= DistEsti (BasicDF L) by Th1;
then {} in DistEsti (BasicDF L) by ORDINAL1:33;
then A55: {} in dom q by LATTICE5:28;
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 LATTICE5:def 14;
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 9;
Quadr2 q,{} = [u,v,a,b] by A55, A56, Def7;
then A59: b = Q `4 by MCART_1:def 11;
(S . 1) `2 = NextDelta2 q by A51, A53, MCART_1:def 2;
then A60: NextDelta2 q c= FD by A54, ZFMISC_1:92;
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 the carrier of (Image f) & e <> id FS )
e in rng f by A46, A57, FUNCT_1:def 5;
hence e in the carrier of (Image f) by YELLOW_0:def 15; :: thesis: e <> id FS
A63: (S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
(S . 1) `1 = NextSet2 (BasicDF L) by A51, A52, MCART_1:def 1;
then A64: NextSet2 (BasicDF L) c= FS by A63, ZFMISC_1:92;
new_set2 the carrier of L = new_set2 (ConsecutiveSet2 the carrier of L,{} ) by Th15
.= ConsecutiveSet2 the carrier of L,(succ {} ) by Th16 ;
then new_set2 the carrier of L c= NextSet2 (BasicDF L) by Th1, Th22;
then A65: new_set2 the carrier of L c= FS by A64, XBOOLE_1:1;
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 Th15, Th19;
ConsecutiveDelta2 q,(succ {} ) = new_bi_fun2 (BiFun (ConsecutiveDelta2 q,{} ),(ConsecutiveSet2 the carrier of L,{} ),L),(Quadr2 q,{} ) by Th20
.= new_bi_fun2 (BasicDF L),Q by A68, LATTICE5:def 16 ;
then new_bi_fun2 (BasicDF L),Q c= NextDelta2 q by Th1, Th25;
then A69: new_bi_fun2 (BasicDF L),Q c= FD by A60, XBOOLE_1:1;
( 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:106;
then FD . W,V = (new_bi_fun2 (BasicDF L),Q) . {the carrier of L},{{the carrier of L}} by A69, GRFUNC_1:8
.= (((BasicDF L) . (Q `1 ),(Q `2 )) "\/" (Q `3 )) "/\" (Q `4 ) by Def5 ;
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: verum
end;
A70: now
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: contradiction
then consider x being set such that
A72: FS = {x} by REALSET1:def 4;
A73: ( [:{x},{x}:] = {[x,x]} & id {x} = {[x,x]} ) by SYSREL:30, ZFMISC_1:35;
field e = {x} by A72, EQREL_1:16;
then id FS c= e by A72, RELAT_2:17;
hence contradiction by A72, A71, A73, XBOOLE_0:def 10; :: thesis: verum
end;
BasicDF L is onto by LATTICE5:43;
then A74: 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: ( w in the carrier of L implies ex z being set st
( z in [:FS,FS:] & w = FD . z ) )
A75: (S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
A76: (S . 0 ) `2 in { ((S . i) `2 ) where i is Element of NAT : verum } ;
A77: S . 0 = [the carrier of L,(BasicDF L)] by Def12;
then BasicDF L = (S . 0 ) `2 by MCART_1:def 2;
then A78: BasicDF L c= FD by A76, ZFMISC_1:92;
assume w in the carrier of L ; :: thesis: ex z being set st
( z in [:FS,FS:] & w = FD . z )
then consider z being set such that
A79: z in [:the carrier of L,the carrier of L:] and
A80: (BasicDF L) . z = w by A74, FUNCT_2:17;
take z ; :: thesis: ( z in [:FS,FS:] & w = FD . z )
the carrier of L = (S . 0 ) `1 by A77, MCART_1:def 1;
then the carrier of L c= FS by A75, 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 A79; :: thesis: w = FD . z
z in dom (BasicDF L) by A79, FUNCT_2:def 1;
hence w = FD . z by A80, A78, GRFUNC_1:8; :: thesis: verum
end;
then rng FD = the carrier of L by FUNCT_2:16;
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 3 :: thesis: ex f being Homomorphism of L,(EqRelLATT FS) st
( f is one-to-one & Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
reconsider f = f as Homomorphism of L,(EqRelLATT FS) ;
take f ; :: thesis: ( f is one-to-one & Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
thus f is one-to-one by A81, LATTICE5:17; :: thesis: ( Image f is finitely_typed & ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
reconsider FD = FD as distance_function of FS,L ;
thus Image f is finitely_typed :: thesis: ( ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) & type_of (Image f) <= 2 )
proof
take FS ; :: according to LATTICE8:def 2 :: thesis: ( ( for e being set st e in the carrier of (Image f) holds
e is Equivalence_Relation of FS ) & ex o being Element of NAT st
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 = o & x,y are_joint_by F,e1,e2 ) )
thus for e being set st e in the carrier of (Image f) holds
e is Equivalence_Relation of FS :: thesis: ex o being Element of NAT st
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 = o & x,y are_joint_by F,e1,e2 )
proof
let e be set ; :: thesis: ( e in the carrier of (Image f) implies e is Equivalence_Relation of FS )
assume e in the carrier of (Image f) ; :: thesis: e is Equivalence_Relation of FS
then e in rng f by YELLOW_0:def 15;
then consider x being set such that
A82: x in dom f and
A83: e = f . x by FUNCT_1:def 5;
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 9;
hence e is Equivalence_Relation of FS by A83; :: thesis: verum
end;
take 2 + 2 ; :: 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 = 2 + 2 & x,y are_joint_by F,e1,e2 )
thus 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 = 2 + 2 & x,y are_joint_by F,e1,e2 ) by Th35; :: thesis: verum
end;
thus ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS ) :: thesis: type_of (Image f) <= 2
proof
A84: {the carrier of L} <> {{the carrier of L}}
proof
assume {the carrier of L} = {{the carrier of L}} ; :: thesis: contradiction
then {the carrier of L} in {the carrier of L} by TARSKI:def 1;
hence contradiction ; :: thesis: verum
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
A85: Aq9,dq9 is_extension2_of A9,d9 and
A86: S . 0 = [A9,d9] and
A87: S . (0 + 1) = [Aq9,dq9] by Def12;
( A9 = the carrier of L & d9 = BasicDF L ) by A2, A86, ZFMISC_1:33;
then consider q being QuadrSeq of BasicDF L such that
A88: Aq9 = NextSet2 (BasicDF L) and
A89: dq9 = NextDelta2 q by A85, Def11;
ConsecutiveSet2 the carrier of L,{} = the carrier of L by Th15;
then reconsider Q = Quadr2 q,{} as Element of [:the carrier of L,the carrier of L,the carrier of L,the carrier of L:] ;
A90: (S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum } ;
succ {} c= DistEsti (BasicDF L) by Th1;
then {} in DistEsti (BasicDF L) by ORDINAL1:33;
then A91: {} in dom q by LATTICE5:28;
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 LATTICE5:def 14;
then consider u, v being Element of the carrier of L, a, b being Element of L such that
A92: q . {} = [u,v,a,b] and
(BasicDF L) . u,v <= a "\/" b ;
consider e being Equivalence_Relation of FS such that
A93: e = f . b and
A94: for x, y being Element of FS holds
( [x,y] in e iff FD . x,y <= b ) by LATTICE5:def 9;
Quadr2 q,{} = [u,v,a,b] by A91, A92, Def7;
then A95: b = Q `4 by MCART_1:def 11;
(S . 1) `2 = NextDelta2 q by A87, A89, MCART_1:def 2;
then A96: NextDelta2 q c= FD by A90, ZFMISC_1:92;
A97: {{the carrier of L}} in {{the carrier of L},{{the carrier of L}}} by TARSKI:def 2;
then A98: {{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 the carrier of (Image f) & e <> id FS )
e in rng f by A46, A93, FUNCT_1:def 5;
hence e in the carrier of (Image f) by YELLOW_0:def 15; :: thesis: e <> id FS
A99: (S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum } ;
(S . 1) `1 = NextSet2 (BasicDF L) by A87, A88, MCART_1:def 1;
then A100: NextSet2 (BasicDF L) c= FS by A99, ZFMISC_1:92;
new_set2 the carrier of L = new_set2 (ConsecutiveSet2 the carrier of L,{} ) by Th15
.= ConsecutiveSet2 the carrier of L,(succ {} ) by Th16 ;
then new_set2 the carrier of L c= NextSet2 (BasicDF L) by Th1, Th22;
then A101: new_set2 the carrier of L c= FS by A100, XBOOLE_1:1;
A102: {{the carrier of L}} in new_set2 the carrier of L by A97, XBOOLE_0:def 3;
A103: {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 A101, A102;
A104: ( ConsecutiveSet2 the carrier of L,{} = the carrier of L & ConsecutiveDelta2 q,{} = BasicDF L ) by Th15, Th19;
ConsecutiveDelta2 q,(succ {} ) = new_bi_fun2 (BiFun (ConsecutiveDelta2 q,{} ),(ConsecutiveSet2 the carrier of L,{} ),L),(Quadr2 q,{} ) by Th20
.= new_bi_fun2 (BasicDF L),Q by A104, LATTICE5:def 16 ;
then new_bi_fun2 (BasicDF L),Q c= NextDelta2 q by Th1, Th25;
then A105: new_bi_fun2 (BasicDF L),Q c= FD by A96, XBOOLE_1:1;
( 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 A103, 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 A98, ZFMISC_1:106;
then FD . W,V = (new_bi_fun2 (BasicDF L),Q) . {the carrier of L},{{the carrier of L}} by A105, GRFUNC_1:8
.= (((BasicDF L) . (Q `1 ),(Q `2 )) "\/" (Q `3 )) "/\" (Q `4 ) by Def5 ;
then FD . W,V <= b by A95, YELLOW_0:23;
then [{the carrier of L},{{the carrier of L}}] in e by A94;
hence e <> id FS by A84, RELAT_1:def 10; :: thesis: verum
end;
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 = 2 + 2 & x,y are_joint_by F,e1,e2 ) by Th35;
hence type_of (Image f) <= 2 by A47, LATTICE5:15; :: thesis: verum