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 14;
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 5;
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:78;
A8: b = (Quadr2 q,o) `4 by A5, A6, MCART_1:78;
A9: y = (Quadr2 q,o) `2 by A5, A6, MCART_1:78;
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:28;
then A11: succ o c= DistEsti d by ORDINAL1:33;
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 16 ;
dom d = [:A,A:] by FUNCT_2:def 1;
then A19: [xo,yo] in dom d by ZFMISC_1:106;
d c= cd by Th24;
then A20: cd . xo,yo = d . x,y by A19, GRFUNC_1:8;
A21: a = (Quadr2 q,o) `3 by A5, A6, MCART_1:78;
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:106;
hence dq . x,z1 = (new_bi_fun2 cd,Q) . x1,{B} by A2, A12, A18, GRFUNC_1:8
.= (cd . xo,xo) "\/" a by A7, A21, Def5
.= (Bottom L) "\/" a by A16, LATTICE5:def 7
.= a by WAYBEL_1:4 ;
:: 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:106;
hence dq . z1,z2 = (new_bi_fun2 cd,Q) . {B},{{B}} by A2, A12, A18, GRFUNC_1:8
.= ((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:106;
hence dq . z2,y = (new_bi_fun2 cd,Q) . {{B}},y1 by A2, A12, A18, GRFUNC_1:8
.= (cd . yo,yo) "\/" a by A9, A21, Def5
.= (Bottom L) "\/" a by A16, LATTICE5:def 7
.= a by WAYBEL_1:4 ;
:: thesis: verum