for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L st d is onto holds
alpha d is one-to-one