theorem :: NORMFORM:37

for A being set
for a being Element of DISJOINT_PAIRS A
for B being Element of Fin (DISJOINT_PAIRS A) st a in mi B holds
a in B by Th36;