theorem :: NORMFORM:38

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