let R be finite set ; :: thesis: for A, B being Subset of R holds JaccardIndex (A,B) = JaccardIndex (B,A)
let A, B be Subset of R; :: thesis: JaccardIndex (A,B) = JaccardIndex (B,A)

per cases ( A \/ B = {} or A \/ B <> {} ) ;

suppose A1: A \/ B = {} ; :: thesis: JaccardIndex (A,B) = JaccardIndex (B,A)

hence JaccardIndex (A,B) = 1 by JacInd
.= JaccardIndex (B,A) by A1, JacInd ;
:: thesis: verum

end;

suppose A1: A \/ B <> {} ; :: thesis: JaccardIndex (A,B) = JaccardIndex (B,A)

hence JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) by JacInd
.= JaccardIndex (B,A) by A1, JacInd ;
:: thesis: verum

end;

end;