take discrete_dist X ; :: thesis: ( discrete_dist X is discerning & discrete_dist X is symmetric & discrete_dist X is Reflexive & discrete_dist X is triangle )
DiscreteSpace X = MetrStruct(# X,(discrete_dist X) #) by METRIC_1:def 11;
hence ( discrete_dist X is discerning & discrete_dist X is symmetric & discrete_dist X is Reflexive & discrete_dist X is triangle ) by METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9; :: thesis: verum