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

hereby :: thesis: ( A = B implies JaccardIndex (A,B) = 1 )

assume T1: JaccardIndex (A,B) = 1 ; :: thesis: A = B

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

suppose A \/ B = {} ; :: thesis: A = B

then ( A = {} & B = {} ) ;
hence A = B ; :: thesis: verum

end;

suppose A \/ B <> {} ; :: thesis: A = B

then JaccardIndex (A,B) = (card (A /\ B)) / (card (A \/ B)) by JacInd;
then card (A /\ B) = card (A \/ B) by XCMPLX_1:58, T1;
hence A = B by LemmaCard; :: thesis: verum

end;

end;

end;

assume A0: A = B ; :: thesis: JaccardIndex (A,B) = 1

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

suppose A = {} ; :: thesis: JaccardIndex (A,B) = 1

then A \/ B = {} by A0;
hence JaccardIndex (A,B) = 1 by JacInd; :: thesis: verum

end;

suppose B1: A <> {} ; :: thesis: JaccardIndex (A,B) = 1

then JaccardIndex (A,B) = (card (A /\ A)) / (card (A \/ A)) by JacInd, A0
.= (card A) / (card A) ;
hence JaccardIndex (A,B) = 1 by B1, XCMPLX_1:60; :: thesis: verum

end;

end;