let L be lower-bounded modular LATTICE; :: thesis: for S being ExtensionSeq2 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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
let S be ExtensionSeq2 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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a ) )
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 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
(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_extension2_of A1,d1 and
A8: S . k = [A1,d1] and
A9: S . (k + 1) = [Aq1,dq1] by Def12;
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:92;
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:92;
(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:92;
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_extension2_of A2,d2 and
A20: S . l = [A2,d2] and
A21: S . (l + 1) = [Aq2,dq2] by Def12;
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:92;
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:92;
(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:92;

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

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

then A1 c= A2 by A12, A24, Th31;
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, Th31, 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 A29: FD . x,y = d2 . [x9,y9] by A23, GRFUNC_1:8
.= d2 . x9,y9 ;
then consider z1, z2 being Element of Aq2 such that
A30: dq2 . x,z1 = a and
A31: dq2 . z1,z2 = ((d2 . x9,y9) "\/" a) "/\" b and
A32: dq2 . z2,y = a by A3, A19, Th30;
( z1 in Aq2 & z2 in Aq2 ) ;
then reconsider z19 = z1, z29 = z2 as Element of FS by A26;
take z19 ; :: thesis: ex z2 being Element of FS st
( FD . x,z19 = a & FD . z19,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )
take z29 ; :: thesis: ( FD . x,z19 = a & FD . z19,z29 = ((FD . x,y) "\/" a) "/\" b & FD . z29,y = a )
A33: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
hence FD . x,z19 = dq2 . [x99,z1] by A27, GRFUNC_1:8
.= a by A30 ;
:: thesis: ( FD . z19,z29 = ((FD . x,y) "\/" a) "/\" b & FD . z29,y = a )
thus FD . z19,z29 = dq2 . [z1,z2] by A27, A33, GRFUNC_1:8
.= ((FD . x,y) "\/" a) "/\" b by A29, A31 ; :: thesis: FD . z29,y = a
thus FD . z29,y = dq2 . [z2,y99] by A27, A33, GRFUNC_1:8
.= a by A32 ; :: thesis: verum

end;

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

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

end;

end;