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;
A1:
BasicDF L is onto
by LATTICE5:43;
consider S being ExtensionSeq2 of the carrier of L, BasicDF L;
A2:
S . 0 = [the carrier of L,(BasicDF L)]
by Def12;
then A3:
(S . 0 ) `1 = the carrier of L
by MCART_1:def 1;
set FS = union { ((S . i) `1 ) where i is Element of NAT : verum } ;
(S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then A4:
the carrier of L c= union { ((S . i) `1 ) where i is Element of NAT : verum }
by A3, ZFMISC_1:92;
reconsider FS = union { ((S . i) `1 ) where i is Element of NAT : verum } as non empty set by A4;
reconsider FD = union { ((S . i) `2 ) where i is Element of NAT : verum } as distance_function of FS,L by Th33;
A6:
FD is onto
proof
A7:
rng (BasicDF L) = the
carrier of
L
by A1, 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 ) )
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 A8:
z in [:the carrier of L,the carrier of L:]
and A9:
(BasicDF L) . z = w
by A7, FUNCT_2:17;
take
z
;
:: thesis: ( z in [:FS,FS:] & w = FD . z )
A10:
S . 0 = [the carrier of L,(BasicDF L)]
by Def12;
then A11:
the
carrier of
L = (S . 0 ) `1
by MCART_1:def 1;
(S . 0 ) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then
the
carrier of
L c= FS
by A11, 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 A8;
:: thesis: w = FD . z
A12:
z in dom (BasicDF L)
by A8, FUNCT_2:def 1;
A13:
BasicDF L = (S . 0 ) `2
by A10, MCART_1:def 2;
(S . 0 ) `2 in { ((S . i) `2 ) where i is Element of NAT : verum }
;
then
BasicDF L c= FD
by A13, ZFMISC_1:92;
hence
w = FD . z
by A9, A12, GRFUNC_1:8;
:: thesis: verum
end;
then
rng FD = the
carrier of
L
by FUNCT_2:16;
hence
FD is
onto
by FUNCT_2:def 3;
:: thesis: verum
end;
alpha FD is join-preserving
proof
let a,
b be
Element of
L;
:: according to WAYBEL_0:def 35 :: thesis: alpha FD preserves_sup_of {a,b}
set f =
alpha FD;
A14:
ex_sup_of (alpha FD) .: {a,b},
EqRelLATT FS
by YELLOW_0:17;
A15:
dom (alpha FD) = the
carrier of
L
by FUNCT_2:def 1;
consider e1 being
Equivalence_Relation of
FS such that A16:
e1 = (alpha FD) . a
and A17:
for
x,
y being
Element of
FS holds
(
[x,y] in e1 iff
FD . x,
y <= a )
by LATTICE5:def 9;
consider e2 being
Equivalence_Relation of
FS such that A18:
e2 = (alpha FD) . b
and A19:
for
x,
y being
Element of
FS holds
(
[x,y] in e2 iff
FD . x,
y <= b )
by LATTICE5:def 9;
consider e3 being
Equivalence_Relation of
FS such that A20:
e3 = (alpha FD) . (a "\/" b)
and A21:
for
x,
y being
Element of
FS holds
(
[x,y] in e3 iff
FD . x,
y <= a "\/" b )
by LATTICE5:def 9;
A22:
field e1 = FS
by ORDERS_1:97;
A23:
field e2 = FS
by ORDERS_1:97;
A24:
field e3 = FS
by ORDERS_1:97;
A25:
e1 "\/" e2 c= e3
proof
now let x,
y be
set ;
:: thesis: ( [x,y] in e1 implies [x,y] in e3 )assume A26:
[x,y] in e1
;
:: thesis: [x,y] in e3then reconsider x' =
x,
y' =
y as
Element of
FS by A22, RELAT_1:30;
A27:
FD . x',
y' <= a
by A17, A26;
a <= a "\/" b
by YELLOW_0:22;
then
FD . x',
y' <= a "\/" b
by A27, ORDERS_2:26;
hence
[x,y] in e3
by A21;
:: thesis: verum end;
then A28:
e1 c= e3
by RELAT_1:def 3;
now let x,
y be
set ;
:: thesis: ( [x,y] in e2 implies [x,y] in e3 )assume A29:
[x,y] in e2
;
:: thesis: [x,y] in e3then reconsider x' =
x,
y' =
y as
Element of
FS by A23, RELAT_1:30;
A30:
FD . x',
y' <= b
by A19, A29;
b <= b "\/" a
by YELLOW_0:22;
then
FD . x',
y' <= b "\/" a
by A30, ORDERS_2:26;
hence
[x,y] in e3
by A21;
:: thesis: verum end;
then
e2 c= e3
by RELAT_1:def 3;
then
e1 \/ e2 c= e3
by A28, XBOOLE_1:8;
hence
e1 "\/" e2 c= e3
by EQREL_1:def 3;
:: thesis: verum
end;
A31:
e3 c= e1 "\/" e2
proof
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 )
assume A32:
[u,v] in e3
;
:: thesis: [u,v] in e1 "\/" e2
then reconsider x =
u,
y =
v as
Element of
FS by A24, RELAT_1:30;
A33:
u in FS
by A24, A32, RELAT_1:30;
A34:
FD . x,
y <= a "\/" b
by A21, A32;
then consider z1,
z2 being
Element of
FS such that A35:
FD . x,
z1 = a
and A36:
FD . z1,
z2 = ((FD . x,y) "\/" a) "/\" b
and A37:
FD . z2,
y = a
by Th34;
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 ) );
A39:
for
m being
Nat st
m in Seg 4 holds
ex
w being
set st
S1[
m,
w]
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(A39);
then consider h being
FinSequence such that A45:
dom h = Seg 4
and A46:
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 ) )
;
Seg 4
= { n where n is Element of NAT : ( 1 <= n & n <= 4 ) }
by FINSEQ_1:def 1;
then A47:
( 1
in Seg 4 & 2
in Seg 4 & 3
in Seg 4 & 4
in Seg 4 )
;
A48:
len h = 4
by A45, FINSEQ_1:def 3;
A49:
u = h . 1
by A46, A47;
A50:
v =
h . 4
by A46, A47
.=
h . (len h)
by A45, FINSEQ_1:def 3
;
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 A51:
( 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 A48, A51, Lm4;
suppose A53:
j = 2
;
:: thesis: [(h . j),(h . (j + 1))] in e1 \/ e2
(FD . x,y) "\/" a <= (a "\/" b) "\/" a
by A34, 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 A19, A36;
then
[(h . 2),z2] in e2
by A46, A47;
then
[(h . 2),(h . 3)] in e2
by A46, A47;
hence
[(h . j),(h . (j + 1))] in e1 \/ e2
by A53, XBOOLE_0:def 3;
:: thesis: verum end;
end;
hence
[u,v] in e1 "\/" e2
by A33, A48, A49, A50, EQREL_1:36;
:: thesis: verum
end;
hence
e3 c= e1 "\/" e2
by RELAT_1:def 3;
:: thesis: verum
end;
sup ((alpha FD) .: {a,b}) =
sup {((alpha FD) . a),((alpha FD) . b)}
by A15, FUNCT_1:118
.=
((alpha FD) . a) "\/" ((alpha FD) . b)
by YELLOW_0:41
.=
e1 "\/" e2
by A16, A18, LATTICE5:10
.=
(alpha FD) . (a "\/" b)
by A20, A25, A31, XBOOLE_0:def 10
.=
(alpha FD) . (sup {a,b})
by YELLOW_0:41
;
hence
alpha FD preserves_sup_of {a,b}
by A14, WAYBEL_0:def 31;
:: thesis: verum
end;
then reconsider f = alpha FD as Homomorphism of L,(EqRelLATT FS) by LATTICE5:16;
A55:
dom f = the carrier of L
by FUNCT_2:def 1;
A56:
ex e being Equivalence_Relation of FS st
( e in the carrier of (Image f) & e <> id FS )
proof
consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq' being non
empty set ,
dq' being
distance_function of
Aq',
L such that A57:
Aq',
dq' is_extension2_of A',
d'
and A58:
(
S . 0 = [A',d'] &
S . (0 + 1) = [Aq',dq'] )
by Def12;
(
A' = the
carrier of
L &
d' = BasicDF L )
by A2, A58, ZFMISC_1:33;
then consider q being
QuadrSeq of
BasicDF L such that A59:
Aq' = NextSet2 (BasicDF L)
and A60:
dq' = NextDelta2 q
by A57, Def11;
A61:
(S . 1) `2 = NextDelta2 q
by A58, A60, MCART_1:def 2;
(S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum }
;
then A62:
NextDelta2 q c= FD
by A61, ZFMISC_1:92;
A63:
(S . 1) `1 = NextSet2 (BasicDF L)
by A58, A59, MCART_1:def 1;
(S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then A64:
NextSet2 (BasicDF L) c= FS
by A63, ZFMISC_1:92;
succ {} c= DistEsti (BasicDF L)
by Th1;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:33;
then A65:
{} in dom q
by LATTICE5:28;
then
q . {} in rng q
by FUNCT_1:def 5;
then
q . {} in { [u,v,a',b'] where u, v is Element of the carrier of L, a', b' is Element of L : (BasicDF L) . u,v <= a' "\/" b' }
by LATTICE5:def 14;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A66:
(
q . {} = [u,v,a,b] &
(BasicDF L) . u,
v <= a "\/" b )
;
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:] ;
A67:
Quadr2 q,
{} = [u,v,a,b]
by A65, A66, Def7;
consider e being
Equivalence_Relation of
FS such that A68:
e = f . b
and A69:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . x,
y <= b )
by LATTICE5:def 9;
take
e
;
:: thesis: ( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A55, A68, FUNCT_1:def 5;
hence
e in the
carrier of
(Image f)
by YELLOW_0:def 15;
:: thesis: e <> id FS
new_set2 the
carrier of
L =
new_set2 (ConsecutiveSet2 the carrier of L,{} )
by Th15
.=
ConsecutiveSet2 the
carrier of
L,
(succ {} )
by Th16
;
then A70:
new_set2 the
carrier of
L c= NextSet2 (BasicDF L)
by Th1, Th22;
A71:
(
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 A71, LATTICE5:def 16
;
then
new_bi_fun2 (BasicDF L),
Q c= NextDelta2 q
by Th1, Th25;
then A72:
new_bi_fun2 (BasicDF L),
Q c= FD
by A62, XBOOLE_1:1;
A73:
new_set2 the
carrier of
L c= FS
by A64, A70, XBOOLE_1:1;
A74:
dom (new_bi_fun2 (BasicDF L),Q) = [:(new_set2 the carrier of L),(new_set2 the carrier of L):]
by FUNCT_2:def 1;
A75:
{the carrier of L} in {{the carrier of L},{{the carrier of L}}}
by TARSKI:def 2;
then A76:
{the carrier of L} in the
carrier of
L \/ {{the carrier of L},{{the carrier of L}}}
by XBOOLE_0:def 3;
A77:
{the carrier of L} in new_set2 the
carrier of
L
by A75, XBOOLE_0:def 3;
A78:
{{the carrier of L}} in {{the carrier of L},{{the carrier of L}}}
by TARSKI:def 2;
then A79:
{{the carrier of L}} in the
carrier of
L \/ {{the carrier of L},{{the carrier of L}}}
by XBOOLE_0:def 3;
A80:
{{the carrier of L}} in new_set2 the
carrier of
L
by A78, XBOOLE_0:def 3;
A81:
[{the carrier of L},{{the carrier of L}}] in dom (new_bi_fun2 (BasicDF L),Q)
by A74, A77, A79, ZFMISC_1:106;
A82:
b = Q `4
by A67, MCART_1:def 11;
reconsider W =
{the carrier of L},
V =
{{the carrier of L}} as
Element of
FS by A73, A76, A80;
FD . W,
V =
(new_bi_fun2 (BasicDF L),Q) . {the carrier of L},
{{the carrier of L}}
by A72, A81, GRFUNC_1:8
.=
(((BasicDF L) . (Q `1 ),(Q `2 )) "\/" (Q `3 )) "/\" (Q `4 )
by Def5
;
then
FD . W,
V <= b
by A82, YELLOW_0:23;
then A83:
[{the carrier of L},{{the carrier of L}}] in e
by A69;
{the carrier of L} <> {{the carrier of L}}
hence
e <> id FS
by A83, RELAT_1:def 10;
:: thesis: verum
end;
FS is non trivial set
proof
now assume A84:
FS is
trivial
;
:: thesis: contradictionconsider x being
set such that A85:
FS = {x}
by A84, REALSET1:def 4;
consider e being
Equivalence_Relation of
FS such that A86:
(
e in the
carrier of
(Image f) &
e <> id FS )
by A56;
field e = {x}
by A85, EQREL_1:16;
then A87:
id FS c= e
by A85, RELAT_2:17;
A88:
[:{x},{x}:] = {[x,x]}
by ZFMISC_1:35;
id {x} = {[x,x]}
by SYSREL:30;
hence
contradiction
by A85, A86, A87, A88, XBOOLE_0:def 10;
:: thesis: verum end;
hence
FS is non
trivial set
;
:: thesis: verum
end;
then reconsider FS = FS as non trivial set ;
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 A6, 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 )
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) <= 2proof
consider A' being non
empty set ,
d' being
distance_function of
A',
L,
Aq' being non
empty set ,
dq' being
distance_function of
Aq',
L such that A92:
Aq',
dq' is_extension2_of A',
d'
and A93:
(
S . 0 = [A',d'] &
S . (0 + 1) = [Aq',dq'] )
by Def12;
(
A' = the
carrier of
L &
d' = BasicDF L )
by A2, A93, ZFMISC_1:33;
then consider q being
QuadrSeq of
BasicDF L such that A94:
Aq' = NextSet2 (BasicDF L)
and A95:
dq' = NextDelta2 q
by A92, Def11;
A96:
(S . 1) `2 = NextDelta2 q
by A93, A95, MCART_1:def 2;
(S . 1) `2 in { ((S . i) `2 ) where i is Element of NAT : verum }
;
then A97:
NextDelta2 q c= FD
by A96, ZFMISC_1:92;
A98:
(S . 1) `1 = NextSet2 (BasicDF L)
by A93, A94, MCART_1:def 1;
(S . 1) `1 in { ((S . i) `1 ) where i is Element of NAT : verum }
;
then A99:
NextSet2 (BasicDF L) c= FS
by A98, ZFMISC_1:92;
succ {} c= DistEsti (BasicDF L)
by Th1;
then
{} in DistEsti (BasicDF L)
by ORDINAL1:33;
then A100:
{} in dom q
by LATTICE5:28;
then
q . {} in rng q
by FUNCT_1:def 5;
then
q . {} in { [u,v,a',b'] where u, v is Element of the carrier of L, a', b' is Element of L : (BasicDF L) . u,v <= a' "\/" b' }
by LATTICE5:def 14;
then consider u,
v being
Element of the
carrier of
L,
a,
b being
Element of
L such that A101:
(
q . {} = [u,v,a,b] &
(BasicDF L) . u,
v <= a "\/" b )
;
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:] ;
A102:
Quadr2 q,
{} = [u,v,a,b]
by A100, A101, Def7;
consider e being
Equivalence_Relation of
FS such that A103:
e = f . b
and A104:
for
x,
y being
Element of
FS holds
(
[x,y] in e iff
FD . x,
y <= b )
by LATTICE5:def 9;
take
e
;
:: thesis: ( e in the carrier of (Image f) & e <> id FS )
e in rng f
by A55, A103, FUNCT_1:def 5;
hence
e in the
carrier of
(Image f)
by YELLOW_0:def 15;
:: thesis: e <> id FS
new_set2 the
carrier of
L =
new_set2 (ConsecutiveSet2 the carrier of L,{} )
by Th15
.=
ConsecutiveSet2 the
carrier of
L,
(succ {} )
by Th16
;
then A105:
new_set2 the
carrier of
L c= NextSet2 (BasicDF L)
by Th1, Th22;
A106:
(
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 A106, LATTICE5:def 16
;
then
new_bi_fun2 (BasicDF L),
Q c= NextDelta2 q
by Th1, Th25;
then A107:
new_bi_fun2 (BasicDF L),
Q c= FD
by A97, XBOOLE_1:1;
A108:
new_set2 the
carrier of
L c= FS
by A99, A105, XBOOLE_1:1;
A109:
dom (new_bi_fun2 (BasicDF L),Q) = [:(new_set2 the carrier of L),(new_set2 the carrier of L):]
by FUNCT_2:def 1;
A110:
{the carrier of L} in {{the carrier of L},{{the carrier of L}}}
by TARSKI:def 2;
then A111:
{the carrier of L} in the
carrier of
L \/ {{the carrier of L},{{the carrier of L}}}
by XBOOLE_0:def 3;
A112:
{the carrier of L} in new_set2 the
carrier of
L
by A110, XBOOLE_0:def 3;
A113:
{{the carrier of L}} in {{the carrier of L},{{the carrier of L}}}
by TARSKI:def 2;
then A114:
{{the carrier of L}} in the
carrier of
L \/ {{the carrier of L},{{the carrier of L}}}
by XBOOLE_0:def 3;
A115:
{{the carrier of L}} in new_set2 the
carrier of
L
by A113, XBOOLE_0:def 3;
A116:
[{the carrier of L},{{the carrier of L}}] in dom (new_bi_fun2 (BasicDF L),Q)
by A109, A112, A114, ZFMISC_1:106;
A117:
b = Q `4
by A102, MCART_1:def 11;
reconsider W =
{the carrier of L},
V =
{{the carrier of L}} as
Element of
FS by A108, A111, A115;
FD . W,
V =
(new_bi_fun2 (BasicDF L),Q) . {the carrier of L},
{{the carrier of L}}
by A107, A116, GRFUNC_1:8
.=
(((BasicDF L) . (Q `1 ),(Q `2 )) "\/" (Q `3 )) "/\" (Q `4 )
by Def5
;
then
FD . W,
V <= b
by A117, YELLOW_0:23;
then A118:
[{the carrier of L},{{the carrier of L}}] in e
by A104;
{the carrier of L} <> {{the carrier of L}}
hence
e <> id FS
by A118, 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 A56, LATTICE5:15; :: thesis: verum