let X be set ; :: thesis: ( proj1 X = {} iff proj2 X = {} )
( ( proj1 X = {} or proj2 X = {} ) implies for x, y being object holds not [x,y] in X ) by XTUPLE_0:def 12, XTUPLE_0:def 13;
hence ( proj1 X = {} iff proj2 X = {} ) by Th8; :: thesis: verum