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: (discrete_dist A) . (x,y) >= 0

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: (discrete_dist A) . (x,y) >= 0

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

end;

suppose x <> y ; :: thesis: (discrete_dist A) . (x,y) >= 0

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

end;

end;

end;

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