theorem :: FUNCT_5:15

for X being set st ( proj1 X = {} or proj2 X = {} ) holds
for x, y being object holds not [x,y] in X by XTUPLE_0:def 12, XTUPLE_0:def 13;