theorem Th54: :: NORMFORM:54

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