theorem :: NORMFORM:29

for X being set
for x being Element of [:(Fin X),(Fin X):] st x `1 misses x `2 holds
x is Element of DISJOINT_PAIRS X by Th23;