theorem Th47: :: NORMFORM:47

for A being set
for B, C being Element of Fin (DISJOINT_PAIRS A) holds mi (B ^ C) c= (mi B) ^ C