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 ;
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 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 ; :: 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 )
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 ;
:: thesis: ( 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 ;
:: thesis: ( 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 ;
:: thesis: 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 ;
:: thesis: verum