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