:: deftheorem defines SymDifMetrSpace ROUGHIF2:def 12 :
for X being finite set holds SymDifMetrSpace X = MetrStruct(# (bool X),(SymmetricDiffDist X) #);