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_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
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_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
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_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
let Aq be non empty set ; :: thesis: for dq being distance_function of Aq,L st Aq,dq is_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
let dq be distance_function of Aq,L; :: thesis: ( Aq,dq is_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b ) )
assume Aq,dq is_extension_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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
then consider q being QuadrSeq of d such that
A1: Aq = NextSet d and
A2: dq = NextDelta q by Def20;
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, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
let a, b be Element of L; :: thesis: ( d . x,y <= a "\/" b implies ex z1, z2, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b ) )
assume A3: d . x,y <= a "\/" b ; :: thesis: ex z1, z2, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
rng q = { [x',y',a',b'] where x', y' is Element of A, a', b' is Element of L : d . x',y' <= a' "\/" b' } by Def14;
then [x,y,a,b] in rng q by A3;
then consider o being set such that
A4: ( o in dom q & q . o = [x,y,a,b] ) by FUNCT_1:def 5;
reconsider o = o as Ordinal by A4;
A5: q . o = Quadr q,o by A4, Def15;
then A6: x = (Quadr q,o) `1 by A4, MCART_1:78;
A7: y = (Quadr q,o) `2 by A4, A5, MCART_1:78;
A8: a = (Quadr q,o) `3 by A4, A5, MCART_1:78;
A9: b = (Quadr q,o) `4 by A4, A5, MCART_1:78;
reconsider B = ConsecutiveSet A,o as non empty set ;
reconsider Q = Quadr q,o as Element of [:B,B,the carrier of L,the carrier of L:] ;
reconsider cd = ConsecutiveDelta q,o as BiFunction of B,L ;
( x in A & y in A & A c= B ) by Th27;
then reconsider xo = x, yo = y as Element of B ;
( xo in B & yo in B & B c= new_set B ) by XBOOLE_1:7;
then reconsider x1 = xo, y1 = yo as Element of new_set B ;
A10: ConsecutiveSet A,(succ o) = new_set B by Th25;
o in DistEsti d by A4, Th28;
then A11: succ o c= DistEsti d by ORDINAL1:33;
then A12: ConsecutiveDelta q,(succ o) c= ConsecutiveDelta q,(DistEsti d) by Th35;
A13: ConsecutiveDelta q,(succ o) = new_bi_fun (BiFun (ConsecutiveDelta q,o),(ConsecutiveSet A,o),L),(Quadr q,o) by Th30
.= new_bi_fun cd,Q by Def16 ;
{B} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A14: {B} in B \/ {{B},{{B}},{{{B}}}} by XBOOLE_0:def 3;
A15: {{B}} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A16: {{B}} in B \/ {{B},{{B}},{{{B}}}} by XBOOLE_0:def 3;
A17: {{B}} in new_set B by A15, XBOOLE_0:def 3;
A18: {{{B}}} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A19: {{{B}}} in B \/ {{B},{{B}},{{{B}}}} by XBOOLE_0:def 3;
A20: {{{B}}} in new_set B by A18, XBOOLE_0:def 3;
A21: cd is zeroed by Th36;
A22: dom (new_bi_fun cd,Q) = [:(new_set B),(new_set B):] by FUNCT_2:def 1;
then A23: [x1,{B}] in dom (new_bi_fun cd,Q) by A14, ZFMISC_1:106;
A24: [{{B}},{{{B}}}] in dom (new_bi_fun cd,Q) by A16, A20, A22, ZFMISC_1:106;
A25: [{B},{{B}}] in dom (new_bi_fun cd,Q) by A14, A17, A22, ZFMISC_1:106;
A26: [{{{B}}},y1] in dom (new_bi_fun cd,Q) by A19, A22, ZFMISC_1:106;
new_set B c= ConsecutiveSet A,(DistEsti d) by A10, A11, Th32;
then reconsider z1 = {B}, z2 = {{B}}, z3 = {{{B}}} as Element of Aq by A1, A14, A17, A20;
take z1 ; :: thesis: ex z2, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
take z2 ; :: thesis: ex z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
take z3 ; :: thesis: ( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
thus dq . x,z1 = (new_bi_fun cd,Q) . x1,{B} by A2, A12, A13, A23, GRFUNC_1:8
.= (cd . xo,xo) "\/" a by A6, A8, Def11
.= (Bottom L) "\/" a by A21, Def7
.= a by WAYBEL_1:4 ; :: thesis: ( dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
thus dq . z2,z3 = (new_bi_fun cd,Q) . {{B}},{{{B}}} by A2, A12, A13, A24, GRFUNC_1:8
.= a by A8, Def11 ; :: thesis: ( dq . z1,z2 = b & dq . z3,y = b )
thus dq . z1,z2 = (new_bi_fun cd,Q) . {B},{{B}} by A2, A12, A13, A25, GRFUNC_1:8
.= b by A9, Def11 ; :: thesis: dq . z3,y = b
thus dq . z3,y = (new_bi_fun cd,Q) . {{{B}}},y1 by A2, A12, A13, A26, GRFUNC_1:8
.= (cd . yo,yo) "\/" b by A7, A9, Def11
.= (Bottom L) "\/" b by A21, Def7
.= b by WAYBEL_1:4 ; :: thesis: verum