theorem :: NORMFORM:24

for X being set
for x, y being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds
( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )