let A be non empty set ; :: thesis: 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
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L st d is onto holds
alpha d is one-to-one
let d be distance_function of A,L; :: thesis: ( d is onto implies alpha d is one-to-one )
set f = alpha d;
assume d is onto ; :: thesis: alpha d is one-to-one
then A1: rng d = the carrier of L by FUNCT_2:def 3;
for a, b being Element of L st (alpha d) . a = (alpha d) . b holds
a = b

proof

let a, b be Element of L; :: thesis: ( (alpha d) . a = (alpha d) . b implies a = b )
assume A2: (alpha d) . a = (alpha d) . b ; :: thesis: a = b
consider z1 being object such that
A3: z1 in [:A,A:] and
A4: d . z1 = a by A1, FUNCT_2:11;
consider x1, y1 being object such that
A5: ( x1 in A & y1 in A ) and
A6: z1 = [x1,y1] by A3, ZFMISC_1:def 2;
reconsider x1 = x1, y1 = y1 as Element of A by A5;
consider z2 being object such that
A7: z2 in [:A,A:] and
A8: d . z2 = b by A1, FUNCT_2:11;
consider x2, y2 being object such that
A9: ( x2 in A & y2 in A ) and
A10: z2 = [x2,y2] by A7, ZFMISC_1:def 2;
reconsider x2 = x2, y2 = y2 as Element of A by A9;
consider E1 being Equivalence_Relation of A such that
A11: E1 = (alpha d) . a and
A12: for x, y being Element of A holds
( [x,y] in E1 iff d . (x,y) <= a ) by Def8;
consider E2 being Equivalence_Relation of A such that
A13: E2 = (alpha d) . b and
A14: for x, y being Element of A holds
( [x,y] in E2 iff d . (x,y) <= b ) by Def8;
A15: d . (x2,y2) = b by A8, A10;
then [x2,y2] in E2 by A14;
then A16: b <= a by A2, A15, A11, A12, A13;
A17: d . (x1,y1) = a by A4, A6;
then [x1,y1] in E1 by A12;
then a <= b by A2, A17, A11, A13, A14;
hence a = b by A16, ORDERS_2:2; :: thesis: verum

end;

hence alpha d is one-to-one by WAYBEL_1:def 1; :: thesis: verum