:: deftheorem Def8 defines alpha LATTICE5:def 8 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for b₄ being Function of L,(EqRelLATT A) holds
( b₄ = alpha d iff for e being Element of L ex E being Equivalence_Relation of A st
( E = b₄ . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) );