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 object ; :: 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) and
A4: e2 in the carrier of (Image f) and
A5: [x,y] in e1 "\/" e2 ; :: thesis:
A6: the carrier of (Image f) = rng f by YELLOW_0:def 15;
then consider a being object such that
A7: a in dom f and
A8: e1 = f . a by A3, FUNCT_1:def 3;
consider b being object such that
A9: b in dom f and
A10: e2 = f . b by A4, A6, FUNCT_1:def 3;
reconsider a = a, b = b as Element of L by A7, A9;
reconsider a = a, b = b as Element of L ;
consider e being Equivalence_Relation of FS such that
A11: e = f . (a "\/" b) and
A12: for u, v being Element of FS holds
( [u,v] in e iff FD . (u,v) <= a "\/" b ) by A1, LATTICE5:def 8;
consider e29 being Equivalence_Relation of FS such that
A13: e29 = f . b and
A14: for u, v being Element of FS holds
( [u,v] in e29 iff FD . (u,v) <= b ) by A1, LATTICE5:def 8;
consider e19 being Equivalence_Relation of FS such that
A15: e19 = f . a and
A16: for u, v being Element of FS holds
( [u,v] in e19 iff FD . (u,v) <= a ) by A1, LATTICE5:def 8;
field (e1 "\/" e2) = FS by ORDERS_1:12;
then reconsider u = x, v = y as Element of FS by A5, RELAT_1:15;
A17: Seg 4 = { n where n is Nat : ( 1 <= n & n <= 4 ) } by FINSEQ_1:def 1;
then A18: 1 in Seg 4 ;
e = (f . a) "\/" (f . b) by A11, WAYBEL_6:2
.= e1 "\/" e2 by A8, A10, LATTICE5:10 ;
then A19: FD . (u,v) <= a "\/" b by A5, A12;
then consider z1, z2 being Element of FS such that
A20: FD . (u,z1) = a and
A21: FD . (z1,z2) = ((FD . (u,v)) "\/" a) "/\" b and
A22: FD . (z2,v) = a by A2, Th33;
defpred S₁[ set , object ] means ( ( $1 = 1 implies $2 = u ) & ( $1 = 2 implies $2 = z1 ) & ( $1 = 3 implies $2 = z2 ) & ( $1 = 4 implies $2 = v ) );
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 = u ) & ( m = 2 implies h . m = z1 ) & ( m = 3 implies h . m = z2 ) & ( m = 4 implies h . m = v ) ) ;
A31: len h = 4 by A29, FINSEQ_1:def 3;
A32: 3 in Seg 4 by A17;
A33: 4 in Seg 4 by A17;
A34: 2 in Seg 4 by A17;
rng h c= FS

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in rng h ; :: thesis:
then consider j being object such that
A35: j in dom h and
A36: w = h . j by FUNCT_1:def 3;

per cases by A29, A35, Lm3;

suppose j = 1 ; :: thesis:

then h . j = u by A30, A18;
hence w in FS by A36; :: thesis:

end;

suppose j = 2 ; :: thesis:

then h . j = z1 by A30, A34;
hence w in FS by A36; :: thesis:

end;

suppose j = 3 ; :: thesis:

then h . j = z2 by A30, A32;
hence w in FS by A36; :: thesis:

end;

suppose j = 4 ; :: thesis:

then h . j = v by A30, A33;
hence w in FS by A36; :: thesis:

end;

then reconsider h = h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A29, FINSEQ_1:def 3;
then reconsider h = h as non empty FinSequence of FS ;
A37: h . 1 = x by A30, A18;
A38: for j being Element of NAT st 1 <= j & j < len h holds
( ( j is odd 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 A39: ( 1 <= j & j < len h ) ; :: thesis:

per cases by A31, A39, Lm4;

suppose A40: j = 1 ; :: thesis:

[u,z1] in e19 by A16, A20;
then [(h . 1),z1] in e19 by A30, A18;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A8, A15, A30, A34, A40; :: thesis:

end;

suppose A41: j = 2 ; :: thesis:

(FD . (u,v)) "\/" a <= (a "\/" b) "\/" a by A19, WAYBEL_1:2;
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:1;
then ((FD . (u,v)) "\/" a) "/\" b <= b by LATTICE3:18;
then [z1,z2] in e29 by A14, A21;
then A42: [(h . 2),z2] in e29 by A30, A34;
consider i being Element of NAT such that
A43: i = 1 ;
2 * i = j by A41, A43;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A10, A13, A30, A32, A41, A42; :: thesis:

end;

suppose A44: j = 3 ; :: thesis:

[z2,v] in e19 by A16, A22;
then A45: [(h . 3),v] in e19 by A30, A32;
consider i being Element of NAT such that
A46: i = 1 ;
(2 * i) + 1 = j by A44, A46;
hence ( ( j is odd implies [(h . j),(h . (j + 1))] in e1 ) & ( j is even implies [(h . j),(h . (j + 1))] in e2 ) ) by A8, A15, A30, A33, A44, A45; :: thesis:

end;

take h ; :: thesis:
thus len h = 2 + 2 by A29, FINSEQ_1:def 3; :: thesis:
h . (len h) = h . 4 by A29, FINSEQ_1:def 3
.= y by A30, A33 ;
hence x,y are_joint_by h,e1,e2 by A37, A38; :: thesis: