set S = DiscreteSpace A;
for x, y being Element of A holds (discrete_dist A) . (x,y) >= 0

proof

let x, y be Element of A; :: thesis:

per cases ;

suppose x = y ; :: thesis:

hence (discrete_dist A) . (x,y) >= 0 by METRIC_1:def 10; :: thesis:

end;

suppose x <> y ; :: thesis:

hence (discrete_dist A) . (x,y) >= 0 by METRIC_1:def 10; :: thesis:

end;

end;

end;

hence ( discrete_dist A is finite & not discrete_dist A is empty & discrete_dist A is nonnegative-yielding ) ; :: thesis: