theorem Th26: :: NORMFORM:26

for X being set
for x being Element of [:(Fin X),(Fin X):]
for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X