:: deftheorem JacDef2 defines JaccardDist ROUGHIF2:def 7 :
for R being finite set
for b₂ being Function of [:(bool R),(bool R):],REAL holds
( b₂ = JaccardDist R iff for A, B being Subset of R holds b₂ . (A,B) = 1 - (JaccardIndex (A,B)) );