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 3;
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:74;
A8: b = (Quadr (q,o)) `4 by A5, A6, MCART_1:74;
A9: y = (Quadr (q,o)) `2 by A5, A6, MCART_1:74;
A10: a = (Quadr (q,o)) `3 by A5, A6, MCART_1:74;
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:21;
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:87;
hence dq . (x,z1) = (new_bi_fun (cd,Q)) . (x1,{B}) by A2, A20, A21, GRFUNC_1:2
.= (cd . (xo,xo)) "\/" a by A7, A10, Def11
.= (Bottom L) "\/" a by A16, Def7
.= a by WAYBEL_1:3 ;
:: 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:87;
hence dq . (z2,z3) = (new_bi_fun (cd,Q)) . ({{B}},{{{B}}}) by A2, A20, A21, GRFUNC_1:2
.= 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:87;
hence dq . (z1,z2) = (new_bi_fun (cd,Q)) . ({B},{{B}}) by A2, A20, A21, GRFUNC_1:2
.= 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:87;
hence dq . (z3,y) = (new_bi_fun (cd,Q)) . ({{{B}}},y1) by A2, A20, A21, GRFUNC_1:2
.= (cd . (yo,yo)) "\/" b by A9, A8, Def11
.= (Bottom L) "\/" b by A16, Def7
.= b by WAYBEL_1:3 ;
:: thesis: verum