let L be lower-bounded modular LATTICE; :: thesis:
let S be ExtensionSeq2 of the carrier of L, BasicDF L; :: thesis:
let FS be non empty set ; :: thesis:
let FD be distance_function of FS,L; :: thesis:
let f be Homomorphism of L,(EqRelLATT FS); :: thesis:
let e1, e2 be Equivalence_Relation of FS; :: thesis:
let x, y be set ; :: thesis:
assume that
A1: f = alpha FD and
A2: ( FS = union { ((S . i) `1 ) where i is Element of NAT : verum } & FD = union { ((S . i) `2 ) where i is Element of NAT : verum } ) and
A3: ( e1 in the carrier of (Image f) & e2 in the carrier of (Image f) ) and
A4: [x,y] in e1 "\/" e2 ; :: thesis:
A5: the carrier of (Image f) = rng f by YELLOW_0:def 15;
then consider a being set such that
A6: a in dom f and
A7: e1 = f . a by A3, FUNCT_1:def 5;
consider b being set such that
A8: b in dom f and
A9: e2 = f . b by A3, A5, FUNCT_1:def 5;
reconsider a = a, b = b as Element of L by A6, A8;
field (e1 "\/" e2) = FS by ORDERS_1:97;
then reconsider u = x, v = y as Element of FS by A4, RELAT_1:30;
reconsider a = a, b = b as Element of L ;
consider e1' being Equivalence_Relation of FS such that
A10: e1' = f . a and
A11: for u, v being Element of FS holds
( [u,v] in e1' iff FD . u,v <= a ) by A1, LATTICE5:def 9;
consider e2' being Equivalence_Relation of FS such that
A12: e2' = f . b and
A13: for u, v being Element of FS holds
( [u,v] in e2' iff FD . u,v <= b ) by A1, LATTICE5:def 9;
consider e being Equivalence_Relation of FS such that
A14: e = f . (a "\/" b) and
A15: for u, v being Element of FS holds
( [u,v] in e iff FD . u,v <= a "\/" b ) by A1, LATTICE5:def 9;
e = (f . a) "\/" (f . b) by A14, WAYBEL_6:2
.= e1 "\/" e2 by A7, A9, LATTICE5:10 ;
then A16: FD . u,v <= a "\/" b by A4, A15;
then consider z1, z2 being Element of FS such that
A17: FD . u,z1 = a and
A18: FD . z1,z2 = ((FD . u,v) "\/" a) "/\" b and
A19: FD . z2,v = a by A2, Th34;
defpred S₁[ set , set ] means ( ( $1 = 1 implies $2 = u ) & ( $1 = 2 implies $2 = z1 ) & ( $1 = 3 implies $2 = z2 ) & ( $1 = 4 implies $2 = v ) );
A21: for m being Nat st m in Seg 4 holds
ex w being set st S₁[m,w]

proof

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

per cases by A22, Lm3;

suppose A23: m = 1 ; :: thesis:

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

end;

suppose A24: m = 2 ; :: thesis:

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

end;

suppose A25: m = 3 ; :: thesis:

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

end;

suppose A26: m = 4 ; :: thesis:

take w = y; :: thesis:
thus S₁[m,w] by A26; :: 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(A21);
then consider h being FinSequence such that
A27: dom h = Seg 4 and
A28: for m being Nat st m in Seg 4 holds
( ( m = 1 implies h . m = u ) & ( m = 2 implies h . m = z1 ) & ( m = 3 implies h . m = z2 ) & ( m = 4 implies h . m = v ) ) ;
Seg 4 = { n where n is Element of NAT : ( 1 <= n & n <= 4 ) } by FINSEQ_1:def 1;
then A29: ( 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4 ) ;
A30: len h = 4 by A27, FINSEQ_1:def 3;
rng h c= FS

proof

let w be set ; :: according to TARSKI:def 3 :: thesis:
assume w in rng h ; :: thesis:
then consider j being set such that
A31: ( j in dom h & w = h . j ) by FUNCT_1:def 5;

per cases by A27, A31, Lm3;

suppose j = 1 ; :: thesis:

then h . j = u by A28, A29;
hence w in FS by A31; :: thesis:

end;

suppose j = 2 ; :: thesis:

then h . j = z1 by A28, A29;
hence w in FS by A31; :: thesis:

end;

suppose j = 3 ; :: thesis:

then h . j = z2 by A28, A29;
hence w in FS by A31; :: thesis:

end;

suppose j = 4 ; :: thesis:

then h . j = v by A28, A29;
hence w in FS by A31; :: thesis:

end;

then reconsider h = h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A27, FINSEQ_1:def 3;
then reconsider h = h as non empty FinSequence of FS ;
take h ; :: thesis:
thus len h = 2 + 2 by A27, FINSEQ_1:def 3; :: thesis:
A32: h . 1 = x by A28, A29;
A33: h . (len h) = h . 4 by A27, FINSEQ_1:def 3
.= y by A28, A29 ;
for j being Element of NAT st 1 <= j & j < len h holds
( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) )

proof

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

per cases by A30, A34, Lm4;

suppose A35: j = 1 ; :: thesis:

[u,z1] in e1' by A11, A17;
then [(h . 1),z1] in e1' by A28, A29;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A7, A10, A28, A29, A35; :: thesis:

end;

suppose A36: j = 2 ; :: thesis:

consider i being Element of NAT such that
A37: i = 1 ;
A38: 2 * i = j by A36, A37;
(FD . u,v) "\/" a <= (a "\/" b) "\/" a by A16, WAYBEL_1:3;
then (FD . u,v) "\/" a <= b "\/" (a "\/" a) by LATTICE3:14;
then (FD . u,v) "\/" a <= b "\/" a by YELLOW_5:1;
then ((FD . u,v) "\/" a) "/\" b <= b "/\" (b "\/" a) by WAYBEL_1:2;
then ((FD . u,v) "\/" a) "/\" b <= b by LATTICE3:18;
then [z1,z2] in e2' by A13, A18;
then [(h . 2),z2] in e2' by A28, A29;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A9, A12, A28, A29, A36, A38; :: thesis:

end;

suppose A39: j = 3 ; :: thesis:

consider i being Element of NAT such that
A40: i = 1 ;
A41: (2 * i) + 1 = j by A39, A40;
[z2,v] in e1' by A11, A19;
then [(h . 3),v] in e1' by A28, A29;
hence ( ( not j is even implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A7, A10, A28, A29, A39, A41; :: thesis:

end;

hence x,y are_joint_by h,e1,e2 by A32, A33, LATTICE5:def 3; :: thesis: