:: deftheorem defines DiscreteSpace METRIC_1:def 11 :
for A being set holds DiscreteSpace A = MetrStruct(# A,(discrete_dist A) #);