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 = { [x9,y9,a9,b9] where x9, y9 is Element of A, a9, b9 is Element of L : d . x9,y9 <= a9 "\/" b9 } by Def14;
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 = Quadr q,o by A4, Def15;
then A7: x = (Quadr q,o) `1 by A5, MCART_1:78;
A8: b = (Quadr q,o) `4 by A5, A6, MCART_1:78;
A9: y = (Quadr q,o) `2 by A5, A6, MCART_1:78;
A10: a = (Quadr q,o) `3 by A5, A6, MCART_1:78;
reconsider B = ConsecutiveSet A,o as non empty set ;
{B} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A11: {B} in B \/ {{B},{{B}},{{{B}}}} by XBOOLE_0:def 3;
reconsider cd = ConsecutiveDelta q,o as BiFunction of B,L ;
reconsider Q = Quadr q,o as Element of [:B,B,the carrier of L,the carrier of L:] ;
A12: ( x in A & y in A ) ;
A13: {{B}} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A14: {{B}} in new_set B by XBOOLE_0:def 3;
A c= B by Th27;
then reconsider xo = x, yo = y as Element of B by A12;
A15: B c= new_set B by XBOOLE_1:7;
( xo in B & yo in B ) ;
then reconsider x1 = xo, y1 = yo as Element of new_set B by A15;
A16: cd is zeroed by Th36;
A17: {{{B}}} in {{B},{{B}},{{{B}}}} by ENUMSET1:def 1;
then A18: {{{B}}} in new_set B by XBOOLE_0:def 3;
o in DistEsti d by A4, Th28;
then A19: succ o c= DistEsti d by ORDINAL1:33;
then A20: ConsecutiveDelta q,(succ o) c= ConsecutiveDelta q,(DistEsti d) by Th35;
ConsecutiveSet A,(succ o) = new_set B by Th25;
then new_set B c= ConsecutiveSet A,(DistEsti d) by A19, Th32;
then reconsider z1 = {B}, z2 = {{B}}, z3 = {{{B}}} as Element of Aq by A1, A11, A14, A18;
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 )
A21: 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 ;
A22: dom (new_bi_fun cd,Q) = [:(new_set B),(new_set B):] by FUNCT_2:def 1;
then [x1,{B}] in dom (new_bi_fun cd,Q) by A11, ZFMISC_1:106;
hence dq . x,z1 = (new_bi_fun cd,Q) . x1,{B} by A2, A20, A21, GRFUNC_1:8
.= (cd . xo,xo) "\/" a by A7, A10, Def11
.= (Bottom L) "\/" a by A16, Def7
.= a by WAYBEL_1:4 ;
:: thesis: ( dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
{{B}} in B \/ {{B},{{B}},{{{B}}}} by A13, XBOOLE_0:def 3;
then [{{B}},{{{B}}}] in dom (new_bi_fun cd,Q) by A18, A22, ZFMISC_1:106;
hence dq . z2,z3 = (new_bi_fun cd,Q) . {{B}},{{{B}}} by A2, A20, A21, GRFUNC_1:8
.= a by A10, Def11 ;
:: thesis: ( dq . z1,z2 = b & dq . z3,y = b )
[{B},{{B}}] in dom (new_bi_fun cd,Q) by A11, A14, A22, ZFMISC_1:106;
hence dq . z1,z2 = (new_bi_fun cd,Q) . {B},{{B}} by A2, A20, A21, GRFUNC_1:8
.= b by A8, Def11 ;
:: thesis: dq . z3,y = b
{{{B}}} in B \/ {{B},{{B}},{{{B}}}} by A17, XBOOLE_0:def 3;
then [{{{B}}},y1] in dom (new_bi_fun cd,Q) by A22, ZFMISC_1:106;
hence dq . z3,y = (new_bi_fun cd,Q) . {{{B}}},y1 by A2, A20, A21, GRFUNC_1:8
.= (cd . yo,yo) "\/" b by A9, A8, Def11
.= (Bottom L) "\/" b by A16, Def7
.= b by WAYBEL_1:4 ;
:: thesis: verum