let R be finite set ; :: thesis: for A, B being Subset of R holds (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))
let A, B be Subset of R; :: thesis: (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))
per cases ( A \/ B <> {} or A \/ B = {} ) ;
suppose A1: A \/ B <> {} ; :: thesis: (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))
(JaccardDist R) . (A,B) = 1 - (JaccardIndex (A,B)) by JacDef2
.= 1 - ((card (A /\ B)) / (card (A \/ B))) by JacInd, A1
.= (card (A \+\ B)) / (card (A \/ B)) by A1, Lemacik ;
hence (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B)) ; :: thesis: verum
end;
suppose A1: A \/ B = {} ; :: thesis: (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B))
(JaccardDist R) . (A,B) = 1 - (JaccardIndex (A,B)) by JacDef2
.= 1 - 1 by JacInd, A1
.= (card (A \+\ B)) / (card (A \/ B)) by A1 ;
hence (JaccardDist R) . (A,B) = (card (A \+\ B)) / (card (A \/ B)) ; :: thesis: verum
end;
end;