:: deftheorem JacInd defines JaccardIndex ROUGHIF2:def 6 :
for R being finite set
for A, B being Subset of R holds
( ( A \/ B <> {} implies JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) ) & ( not A \/ B <> {} implies JaccardIndex (A,B) = 1 ) );