:: deftheorem defines MarczewskiDistance ROUGHIF2:def 8 :
for R being finite 1-sorted holds MarczewskiDistance R = JaccardDist ([#] R);