let A be non empty set ; 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; 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; 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 ; 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; ( 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
; 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
;
let x, y be 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 a, b be Element of L; ( 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
; 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 Def13;
then
[x,y,a,b] in rng q
by A3;
then consider o being object 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, Def14;
then A7:
x = (Quadr (q,o)) `1_4
by A5;
A8:
b = (Quadr (q,o)) `4_4
by A5, A6;
A9:
y = (Quadr (q,o)) `2_4
by A5, A6;
A10:
a = (Quadr (q,o)) `3_4
by A5, A6;
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:
{{B}} in {{B},{{B}},{{{B}}}}
by ENUMSET1:def 1;
then A13:
{{B}} in new_set B
by XBOOLE_0:def 3;
A c= B
by Th24;
then reconsider xo = x, yo = y as Element of B ;
A14:
B c= new_set B
by XBOOLE_1:7;
reconsider x1 = xo, y1 = yo as Element of new_set B by A14;
A15:
cd is zeroed
by Th33;
A16:
{{{B}}} in {{B},{{B}},{{{B}}}}
by ENUMSET1:def 1;
then A17:
{{{B}}} in new_set B
by XBOOLE_0:def 3;
o in DistEsti d
by A4, Th25;
then A18:
succ o c= DistEsti d
by ORDINAL1:21;
then A19:
ConsecutiveDelta (q,(succ o)) c= ConsecutiveDelta (q,(DistEsti d))
by Th32;
ConsecutiveSet (A,(succ o)) = new_set B
by Th22;
then
new_set B c= ConsecutiveSet (A,(DistEsti d))
by A18, Th29;
then reconsider z1 = {B}, z2 = {{B}}, z3 = {{{B}}} as Element of Aq by A1, A11, A13, A17;
take
z1
; 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
; 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
; ( dq . (x,z1) = a & dq . (z2,z3) = a & dq . (z1,z2) = b & dq . (z3,y) = b )
A20: ConsecutiveDelta (q,(succ o)) =
new_bi_fun ((BiFun ((ConsecutiveDelta (q,o)),(ConsecutiveSet (A,o)),L)),(Quadr (q,o)))
by Th27
.=
new_bi_fun (cd,Q)
by Def15
;
A21:
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, A19, A20, GRFUNC_1:2
.=
(cd . (xo,xo)) "\/" a
by A7, A10, Def10
.=
(Bottom L) "\/" a
by A15
.=
a
by WAYBEL_1:3
;
( dq . (z2,z3) = a & dq . (z1,z2) = b & dq . (z3,y) = b )
{{B}} in B \/ {{B},{{B}},{{{B}}}}
by A12, XBOOLE_0:def 3;
then
[{{B}},{{{B}}}] in dom (new_bi_fun (cd,Q))
by A17, A21, ZFMISC_1:87;
hence dq . (z2,z3) =
(new_bi_fun (cd,Q)) . ({{B}},{{{B}}})
by A2, A19, A20, GRFUNC_1:2
.=
a
by A10, Def10
;
( dq . (z1,z2) = b & dq . (z3,y) = b )
[{B},{{B}}] in dom (new_bi_fun (cd,Q))
by A11, A13, A21, ZFMISC_1:87;
hence dq . (z1,z2) =
(new_bi_fun (cd,Q)) . ({B},{{B}})
by A2, A19, A20, GRFUNC_1:2
.=
b
by A8, Def10
;
dq . (z3,y) = b
{{{B}}} in B \/ {{B},{{B}},{{{B}}}}
by A16, XBOOLE_0:def 3;
then
[{{{B}}},y1] in dom (new_bi_fun (cd,Q))
by A21, ZFMISC_1:87;
hence dq . (z3,y) =
(new_bi_fun (cd,Q)) . ({{{B}}},y1)
by A2, A19, A20, GRFUNC_1:2
.=
(cd . (yo,yo)) "\/" b
by A9, A8, Def10
.=
(Bottom L) "\/" b
by A15
.=
b
by WAYBEL_1:3
;
verum