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 ) & ( ( for x, y being set holds not [x,y] in X ) implies ( proj1 X = {} & proj2 X = {} ) ) ) by Th17, RELAT_1:def 4, RELAT_1:def 5;
hence ( proj1 X = {} iff proj2 X = {} ) ; :: thesis: verum