let L be lower-bounded LATTICE; :: thesis: for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
let S be ExtensionSeq of the carrier of L, BasicDF L; :: thesis: for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
let FS be non empty set ; :: thesis: for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
let FD be distance_function of FS,L; :: thesis: for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
let x, y be Element of FS; :: thesis: for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
let a, b be Element of L; :: thesis: ( FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b implies ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b ) )
assume that
A1: FS = union { ((S . i) `1) where i is Element of NAT : verum } and
A2: FD = union { ((S . i) `2) where i is Element of NAT : verum } and
A3: FD . (x,y) <= a "\/" b ; :: thesis: ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )
(S . 0) `1 in { ((S . i) `1) where i is Element of NAT : verum } ;
then reconsider X = { ((S . i) `1) where i is Element of NAT : verum } as non empty set ;
consider x1 being set such that
A4: x in x1 and
A5: x1 in X by A1, TARSKI:def 4;
consider k being Element of NAT such that
A6: x1 = (S . k) `1 by A5;
consider A1 being non empty set , d1 being distance_function of A1,L, Aq1 being non empty set , dq1 being distance_function of Aq1,L such that
A7: Aq1,dq1 is_extension_of A1,d1 and
A8: S . k = [A1,d1] and
A9: S . (k + 1) = [Aq1,dq1] by Def21;
A10: x in A1 by A4, A6, A8, MCART_1:def 1;
(S . k) `2 = d1 by A8, MCART_1:def 2;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A11: d1 c= FD by A2, ZFMISC_1:74;
A12: (S . k) `1 = A1 by A8, MCART_1:def 1;
A13: (S . (k + 1)) `1 = Aq1 by A9, MCART_1:def 1;
then Aq1 in { ((S . i) `1) where i is Element of NAT : verum } ;
then A14: Aq1 c= FS by A1, ZFMISC_1:74;
(S . (k + 1)) `2 = dq1 by A9, MCART_1:def 2;
then dq1 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A15: dq1 c= FD by A2, ZFMISC_1:74;
consider y1 being set such that
A16: y in y1 and
A17: y1 in X by A1, TARSKI:def 4;
consider l being Element of NAT such that
A18: y1 = (S . l) `1 by A17;
consider A2 being non empty set , d2 being distance_function of A2,L, Aq2 being non empty set , dq2 being distance_function of Aq2,L such that
A19: Aq2,dq2 is_extension_of A2,d2 and
A20: S . l = [A2,d2] and
A21: S . (l + 1) = [Aq2,dq2] by Def21;
A22: y in A2 by A16, A18, A20, MCART_1:def 1;
(S . l) `2 = d2 by A20, MCART_1:def 2;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A23: d2 c= FD by A2, ZFMISC_1:74;
A24: (S . l) `1 = A2 by A20, MCART_1:def 1;
A25: (S . (l + 1)) `1 = Aq2 by A21, MCART_1:def 1;
then Aq2 in { ((S . i) `1) where i is Element of NAT : verum } ;
then A26: Aq2 c= FS by A1, ZFMISC_1:74;
(S . (l + 1)) `2 = dq2 by A21, MCART_1:def 2;
then dq2 in { ((S . i) `2) where i is Element of NAT : verum } ;
then A27: dq2 c= FD by A2, ZFMISC_1:74;

per cases ( k <= l or l <= k ) ;

suppose k <= l ; :: thesis: ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )

then A1 c= A2 by A12, A24, Th41;
then reconsider x9 = x, y9 = y as Element of A2 by A10, A16, A18, A20, MCART_1:def 1;
A28: ( x9 in A2 & y9 in A2 ) ;
A2 c= Aq2 by A24, A25, Th41, NAT_1:11;
then reconsider x99 = x9, y99 = y9 as Element of Aq2 by A28;
dom d2 = [:A2,A2:] by FUNCT_2:def 1;
then FD . (x,y) = d2 . [x9,y9] by A23, GRFUNC_1:2
.= d2 . (x9,y9) ;
then consider z1, z2, z3 being Element of Aq2 such that
A29: dq2 . (x,z1) = a and
A30: dq2 . (z2,z3) = a and
A31: dq2 . (z1,z2) = b and
A32: dq2 . (z3,y) = b by A3, A19, Th40;
A33: z3 in Aq2 ;
( z1 in Aq2 & z2 in Aq2 ) ;
then reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A26, A33;
take z19 ; :: thesis: ex z2, z3 being Element of FS st
( FD . (x,z19) = a & FD . (z2,z3) = a & FD . (z19,z2) = b & FD . (z3,y) = b )
take z29 ; :: thesis: ex z3 being Element of FS st
( FD . (x,z19) = a & FD . (z29,z3) = a & FD . (z19,z29) = b & FD . (z3,y) = b )
take z39 ; :: thesis: ( FD . (x,z19) = a & FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
A34: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
hence FD . (x,z19) = dq2 . [x99,z1] by A27, GRFUNC_1:2
.= a by A29 ;
:: thesis: ( FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z29,z39) = dq2 . [z2,z3] by A27, A34, GRFUNC_1:2
.= a by A30 ; :: thesis: ( FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z19,z29) = dq2 . [z1,z2] by A27, A34, GRFUNC_1:2
.= b by A31 ; :: thesis: FD . (z39,y) = b
thus FD . (z39,y) = dq2 . [z3,y99] by A27, A34, GRFUNC_1:2
.= b by A32 ; :: thesis: verum

end;

suppose l <= k ; :: thesis: ex z1, z2, z3 being Element of FS st
( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b )

then A2 c= A1 by A12, A24, Th41;
then reconsider x9 = x, y9 = y as Element of A1 by A4, A6, A8, A22, MCART_1:def 1;
A35: ( x9 in A1 & y9 in A1 ) ;
A1 c= Aq1 by A12, A13, Th41, NAT_1:11;
then reconsider x99 = x9, y99 = y9 as Element of Aq1 by A35;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
then FD . (x,y) = d1 . [x9,y9] by A11, GRFUNC_1:2
.= d1 . (x9,y9) ;
then consider z1, z2, z3 being Element of Aq1 such that
A36: dq1 . (x,z1) = a and
A37: dq1 . (z2,z3) = a and
A38: dq1 . (z1,z2) = b and
A39: dq1 . (z3,y) = b by A3, A7, Th40;
A40: z3 in Aq1 ;
( z1 in Aq1 & z2 in Aq1 ) ;
then reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A14, A40;
take z19 ; :: thesis: ex z2, z3 being Element of FS st
( FD . (x,z19) = a & FD . (z2,z3) = a & FD . (z19,z2) = b & FD . (z3,y) = b )
take z29 ; :: thesis: ex z3 being Element of FS st
( FD . (x,z19) = a & FD . (z29,z3) = a & FD . (z19,z29) = b & FD . (z3,y) = b )
take z39 ; :: thesis: ( FD . (x,z19) = a & FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
A41: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
hence FD . (x,z19) = dq1 . [x99,z1] by A15, GRFUNC_1:2
.= a by A36 ;
:: thesis: ( FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z29,z39) = dq1 . [z2,z3] by A15, A41, GRFUNC_1:2
.= a by A37 ; :: thesis: ( FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z19,z29) = dq1 . [z1,z2] by A15, A41, GRFUNC_1:2
.= b by A38 ; :: thesis: FD . (z39,y) = b
thus FD . (z39,y) = dq1 . [z3,y99] by A15, A41, GRFUNC_1:2
.= b by A39 ; :: thesis: verum

end;

end;