let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let d be distance_function of A,L; :: thesis: for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let Aq be non empty set ; :: thesis: for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let dq be distance_function of Aq,L; :: thesis: ( Aq,dq is_extension2_of A,d implies for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a ) )
assume Aq,dq is_extension2_of A,d ; :: thesis: for x, y being Element of A
for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
then consider q being QuadrSeq of d such that
A1: Aq = NextSet2 d and
A2: dq = NextDelta2 q ;
let x, y be Element of A; :: thesis: for a, b being Element of L st d . (x,y) <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
let a, b be Element of L; :: thesis: ( d . (x,y) <= a "\/" b implies ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a ) )
A3: rng q = { [x9,y9,a9,b9] where x9, y9 is Element of A, a9, b9 is Element of L : d . (x9,y9) <= a9 "\/" b9 } by LATTICE5:def 13;
assume d . (x,y) <= a "\/" b ; :: thesis: ex z1, z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
then [x,y,a,b] in rng q by A3;
then consider o being object such that
A4: o in dom q and
A5: q . o = [x,y,a,b] by FUNCT_1:def 3;
reconsider o = o as Ordinal by A4;
A6: q . o = Quadr2 (q,o) by A4, Def6;
then A7: x = (Quadr2 (q,o)) `1_4 by A5;
A8: b = (Quadr2 (q,o)) `4_4 by A5, A6;
A9: y = (Quadr2 (q,o)) `2_4 by A5, A6;
reconsider B = ConsecutiveSet2 (A,o) as non empty set ;
{B} in {{B},{{B}}} by TARSKI:def 2;
then A10: {B} in B \/ {{B},{{B}}} by XBOOLE_0:def 3;
o in DistEsti d by A4, LATTICE5:25;
then A11: succ o c= DistEsti d by ORDINAL1:21;
then A12: ConsecutiveDelta2 (q,(succ o)) c= ConsecutiveDelta2 (q,(DistEsti d)) by Th24;
reconsider cd = ConsecutiveDelta2 (q,o) as BiFunction of B,L ;
reconsider Q = Quadr2 (q,o) as Element of [:B,B, the carrier of L, the carrier of L:] ;
A13: {{B}} in {{B},{{B}}} by TARSKI:def 2;
then A14: {{B}} in new_set2 B by XBOOLE_0:def 3;
ConsecutiveSet2 (A,(succ o)) = new_set2 B by Th15;
then new_set2 B c= ConsecutiveSet2 (A,(DistEsti d)) by A11, Th21;
then reconsider z1 = {B}, z2 = {{B}} as Element of Aq by A1, A10, A14;
take z1 ; :: thesis: ex z2 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
take z2 ; :: thesis: ( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
A15: cd is zeroed by Th25;
A c= B by Th17;
then reconsider xo = x, yo = y as Element of B ;
A16: B c= new_set2 B by XBOOLE_1:7;
reconsider x1 = xo, y1 = yo as Element of new_set2 B by A16;
A17: ConsecutiveDelta2 (q,(succ o)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,o)),(ConsecutiveSet2 (A,o)),L)),(Quadr2 (q,o))) by Th19
.= new_bi_fun2 (cd,Q) by LATTICE5:def 15 ;
dom d = [:A,A:] by FUNCT_2:def 1;
then A18: [xo,yo] in dom d by ZFMISC_1:87;
d c= cd by Th23;
then A19: cd . (xo,yo) = d . (x,y) by A18, GRFUNC_1:2;
A20: a = (Quadr2 (q,o)) `3_4 by A5, A6;
A21: dom (new_bi_fun2 (cd,Q)) = [:(new_set2 B),(new_set2 B):] by FUNCT_2:def 1;
then [x1,{B}] in dom (new_bi_fun2 (cd,Q)) by A10, ZFMISC_1:87;
hence dq . (x,z1) = (new_bi_fun2 (cd,Q)) . (x1,{B}) by A2, A12, A17, GRFUNC_1:2
.= (cd . (xo,xo)) "\/" a by A7, A20, Def4
.= (Bottom L) "\/" a by A15
.= a by WAYBEL_1:3 ;
:: thesis: ( dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )
[{B},{{B}}] in dom (new_bi_fun2 (cd,Q)) by A10, A14, A21, ZFMISC_1:87;
hence dq . (z1,z2) = (new_bi_fun2 (cd,Q)) . ({B},{{B}}) by A2, A12, A17, GRFUNC_1:2
.= ((d . (x,y)) "\/" a) "/\" b by A7, A9, A20, A8, A19, Def4 ;
:: thesis: dq . (z2,y) = a
{{B}} in B \/ {{B},{{B}}} by A13, XBOOLE_0:def 3;
then [{{B}},y1] in dom (new_bi_fun2 (cd,Q)) by A21, ZFMISC_1:87;
hence dq . (z2,y) = (new_bi_fun2 (cd,Q)) . ({{B}},y1) by A2, A12, A17, GRFUNC_1:2
.= (cd . (yo,yo)) "\/" a by A9, A20, Def4
.= (Bottom L) "\/" a by A15
.= a by WAYBEL_1:3 ;
:: thesis: verum