:: deftheorem defines SteinhausMetrSpace ROUGHIF2:def 13 :
for M being non empty finite MetrStruct
for p being Element of M holds SteinhausMetrSpace (M,p) = MetrStruct(# the carrier of M,(SteinhausGen ( the distance of M,p)) #);