for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B \/ (mi C)) = mi (B \/ C) by Th44;