theorem Th27: :: NORMFORM:27

for X being set
for a being Element of DISJOINT_PAIRS X
for x being set holds
( not x in a `1 or not x in a `2 ) by Th23, XBOOLE_0:3;