theorem Th49: :: NORMFORM:49

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