:: deftheorem defines DISJOINT_PAIRS NORMFORM:def 8 :
for X being set holds DISJOINT_PAIRS X = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;