theorem Th23: :: NORMFORM:23

for X being set
for y being Element of [:(Fin X),(Fin X):] holds
( y in DISJOINT_PAIRS X iff y `1 misses y `2 )