set A = the non empty finite set ;
take S = DiscreteSpace the non empty finite set ; :: thesis: ( S is finite & not S is empty & S is with_nonnegative_distance )
S = MetrStruct(# the non empty finite set ,(discrete_dist the non empty finite set ) #) by METRIC_1:def 11;
hence ( S is finite & not S is empty & S is with_nonnegative_distance ) ; :: thesis: verum