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 by Def11;
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 set 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, Def7;
then A7: x = (Quadr2 (q,o)) `1 by A5, MCART_1:74;
A8: b = (Quadr2 (q,o)) `4 by A5, A6, MCART_1:74;
A9: y = (Quadr2 (q,o)) `2 by A5, A6, MCART_1:74;
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 Th25;
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: ( x in A & y in A ) ;
A14: {{B}} in {{B},{{B}}} by TARSKI:def 2;
then A15: {{B}} in new_set2 B by XBOOLE_0:def 3;
ConsecutiveSet2 (A,(succ o)) = new_set2 B by Th16;
then new_set2 B c= ConsecutiveSet2 (A,(DistEsti d)) by A11, Th22;
then reconsider z1 = {B}, z2 = {{B}} as Element of Aq by A1, A10, A15;
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 )
A16: cd is zeroed by Th26;
A c= B by Th18;
then reconsider xo = x, yo = y as Element of B by A13;
A17: B c= new_set2 B by XBOOLE_1:7;
( xo in B & yo in B ) ;
then reconsider x1 = xo, y1 = yo as Element of new_set2 B by A17;
A18: ConsecutiveDelta2 (q,(succ o)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,o)),(ConsecutiveSet2 (A,o)),L)),(Quadr2 (q,o))) by Th20
.= new_bi_fun2 (cd,Q) by LATTICE5:def 15 ;
dom d = [:A,A:] by FUNCT_2:def 1;
then A19: [xo,yo] in dom d by ZFMISC_1:87;
d c= cd by Th24;
then A20: cd . (xo,yo) = d . (x,y) by A19, GRFUNC_1:2;
A21: a = (Quadr2 (q,o)) `3 by A5, A6, MCART_1:74;
A22: 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, A18, GRFUNC_1:2
.= (cd . (xo,xo)) "\/" a by A7, A21, Def5
.= (Bottom L) "\/" a by A16, LATTICE5:def 6
.= 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, A15, A22, ZFMISC_1:87;
hence dq . (z1,z2) = (new_bi_fun2 (cd,Q)) . ({B},{{B}}) by A2, A12, A18, GRFUNC_1:2
.= ((d . (x,y)) "\/" a) "/\" b by A7, A9, A21, A8, A20, Def5 ;
:: thesis: dq . (z2,y) = a
{{B}} in B \/ {{B},{{B}}} by A14, XBOOLE_0:def 3;
then [{{B}},y1] in dom (new_bi_fun2 (cd,Q)) by A22, ZFMISC_1:87;
hence dq . (z2,y) = (new_bi_fun2 (cd,Q)) . ({{B}},y1) by A2, A12, A18, GRFUNC_1:2
.= (cd . (yo,yo)) "\/" a by A9, A21, Def5
.= (Bottom L) "\/" a by A16, LATTICE5:def 6
.= a by WAYBEL_1:3 ;
:: thesis: verum