theorem Th8: :: FUNCT_5:14

for X being set st ( for x, y being object holds not [x,y] in X ) holds
( proj1 X = {} & proj2 X = {} )