theorem Th40: :: NORMFORM:40

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