let X be set ; :: thesis: ( proj1 X = {} iff proj2 X = {} )
( ( proj1 X = {} or proj2 X = {} ) implies for x, y being set holds not [x,y] in X ) by RELAT_1:def 4, RELAT_1:def 5;
hence ( proj1 X = {} iff proj2 X = {} ) by Th17; :: thesis: verum