theorem :: NORMFORM:25

for X being set
for a being Element of DISJOINT_PAIRS X holds a `1 misses a `2 by Th23;