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