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 Def20;
A10: [A1,d1] `1 = A1 ;
A11: x in A1 by A4, A6, A8;
[A1,d1] `2 = d1 ;
then d1 in { ((S . i) `2) where i is Element of NAT : verum } by A8;
then A12: d1 c= FD by A2, ZFMISC_1:74;
A13: [Aq1,dq1] `1 = Aq1 ;
then Aq1 in { ((S . i) `1) where i is Element of NAT : verum } by A9;
then A14: Aq1 c= FS by A1, ZFMISC_1:74;
[Aq1,dq1] `2 = dq1 ;
then dq1 in { ((S . i) `2) where i is Element of NAT : verum } by A9;
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 Def20;
A22: [A2,d2] `1 = A2 ;
A23: y in A2 by A16, A18, A20;
[A2,d2] `2 = d2 ;
then d2 in { ((S . i) `2) where i is Element of NAT : verum } by A20;
then A24: d2 c= FD by A2, ZFMISC_1:74;
A25: [Aq2,dq2] `1 = Aq2 ;
then Aq2 in { ((S . i) `1) where i is Element of NAT : verum } by A21;
then A26: Aq2 c= FS by A1, ZFMISC_1:74;
[Aq2,dq2] `2 = dq2 ;
then dq2 in { ((S . i) `2) where i is Element of NAT : verum } by A21;
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 A10, A22, Th38, A20, A8;
then reconsider x9 = x, y9 = y as Element of A2 by A11, A16, A18, A20;
A2 c= Aq2 by A22, A25, Th38, A20, A21, NAT_1:11;
then reconsider x99 = x9, y99 = y9 as Element of Aq2 ;
dom d2 = [:A2,A2:] by FUNCT_2:def 1;
then FD . (x,y) = d2 . [x9,y9] by A24, GRFUNC_1:2
.= d2 . (x9,y9) ;
then consider z1, z2, z3 being Element of Aq2 such that
A28: dq2 . (x,z1) = a and
A29: dq2 . (z2,z3) = a and
A30: dq2 . (z1,z2) = b and
A31: dq2 . (z3,y) = b by A3, A19, Th37;
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A26;
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 )
A32: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
hence FD . (x,z19) = dq2 . [x99,z1] by A27, GRFUNC_1:2
.= a by A28 ;
:: thesis: ( FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z29,z39) = dq2 . [z2,z3] by A27, A32, GRFUNC_1:2
.= a by A29 ; :: thesis: ( FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z19,z29) = dq2 . [z1,z2] by A27, A32, GRFUNC_1:2
.= b by A30 ; :: thesis: FD . (z39,y) = b
thus FD . (z39,y) = dq2 . [z3,y99] by A27, A32, GRFUNC_1:2
.= b by A31 ; :: 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 A10, A22, Th38, A20, A8;
then reconsider x9 = x, y9 = y as Element of A1 by A4, A6, A8, A23;
A1 c= Aq1 by A10, A13, Th38, A8, A9, NAT_1:11;
then reconsider x99 = x9, y99 = y9 as Element of Aq1 ;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
then FD . (x,y) = d1 . [x9,y9] by A12, GRFUNC_1:2
.= d1 . (x9,y9) ;
then consider z1, z2, z3 being Element of Aq1 such that
A33: dq1 . (x,z1) = a and
A34: dq1 . (z2,z3) = a and
A35: dq1 . (z1,z2) = b and
A36: dq1 . (z3,y) = b by A3, A7, Th37;
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A14;
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 )
A37: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
hence FD . (x,z19) = dq1 . [x99,z1] by A15, GRFUNC_1:2
.= a by A33 ;
:: thesis: ( FD . (z29,z39) = a & FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z29,z39) = dq1 . [z2,z3] by A15, A37, GRFUNC_1:2
.= a by A34 ; :: thesis: ( FD . (z19,z29) = b & FD . (z39,y) = b )
thus FD . (z19,z29) = dq1 . [z1,z2] by A15, A37, GRFUNC_1:2
.= b by A35 ; :: thesis: FD . (z39,y) = b
thus FD . (z39,y) = dq1 . [z3,y99] by A15, A37, GRFUNC_1:2
.= b by A36 ; :: thesis: verum

end;

end;