theorem HoHo: :: ROUGHIF2:3

for x1, x2 being finite set holds (2 * (card (x1 \+\ x2))) / (((card x1) + (card x2)) + (card (x1 \+\ x2))) = (card (x1 \+\ x2)) / (card (x1 \/ x2))