theorem Th46: :: NORMFORM:46

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