for A being 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_extension2_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 being Element of Aq st
( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )