let A, B be finite set ; :: thesis: ( A \/ B <> {} implies 1 - ((card (A /\ B)) / (card (A \/ B))) = (card (A \+\ B)) / (card (A \/ B)) )
assume A1: A \/ B <> {} ; :: thesis: 1 - ((card (A /\ B)) / (card (A \/ B))) = (card (A \+\ B)) / (card (A \/ B))
B1: A /\ B c= A by XBOOLE_1:17;
A c= A \/ B by XBOOLE_1:7;
then B2: A /\ B c= A \/ B by B1;
A \+\ B = (A \/ B) \ (A /\ B) by XBOOLE_1:101;
then B3: card (A \+\ B) = (card (A \/ B)) - (card (A /\ B)) by CARD_2:44, B2;
1 - ((card (A /\ B)) / (card (A \/ B))) = ((card (A \/ B)) / (card (A \/ B))) - ((card (A /\ B)) / (card (A \/ B))) by A1, XCMPLX_1:60
.= (card (A \+\ B)) / (card (A \/ B)) by B3, XCMPLX_1:120 ;
hence 1 - ((card (A /\ B)) / (card (A \/ B))) = (card (A \+\ B)) / (card (A \/ B)) ; :: thesis: verum