for A being set
for a, b being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st B in Normal_forms_on A & a in B & b in B & a c= b holds
a = b