let x1, x2 be finite set ; :: thesis: (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2))) = (card (x1 \+\ x2)) / (card (x1 \/ x2))
set p = card (x1 \/ x2);
set q = ((card x1) + (card x2)) + (card (x1 \+\ x2));
set r = card (x1 \+\ x2);
x1 \/ x2 = x1 \/ (x2 \ x1) by XBOOLE_1:39;
then HH: card (x1 \/ x2) = (card x1) + (card (x2 \ x1)) by XBOOLE_1:79, CARD_2:40;
x1 = (x1 \ x2) \/ (x1 /\ x2) by XBOOLE_1:51;
then g1: card x1 = (card (x1 \ x2)) + (card (x1 /\ x2)) by CARD_2:40, XBOOLE_1:89;
x2 = (x2 \ x1) \/ (x1 /\ x2) by XBOOLE_1:51;
then g2: card x2 = (card (x2 \ x1)) + (card (x1 /\ x2)) by CARD_2:40, XBOOLE_1:89;
((card x1) + (card x2)) + (card (x1 \+\ x2)) = (((card (x1 \ x2)) + (card (x1 /\ x2))) + ((card (x2 \ x1)) + (card (x1 /\ x2)))) + ((card (x1 \ x2)) + (card (x2 \ x1))) by CARD_2:40, XBOOLE_1:82, g1, g2
.= 2 * (card (x1 \/ x2)) by g1, HH ;
hence (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2))) = (card (x1 \+\ x2)) / (card (x1 \/ x2)) by XCMPLX_1:91; :: thesis: verum