let X be set ; :: thesis: ( ( for x, y being set holds not [x,y] in X ) implies ( proj1 X = {} & proj2 X = {} ) )
set x = the Element of proj2 X;
assume A1: for x, y being set holds not [x,y] in X ; :: thesis: ( proj1 X = {} & proj2 X = {} )

hereby :: thesis: proj2 X = {}

set x = the Element of proj1 X;
assume proj1 X <> {} ; :: thesis: contradiction
then ex y being set st [ the Element of proj1 X,y] in X by RELAT_1:def 4;
hence contradiction by A1; :: thesis: verum

end;

assume proj2 X <> {} ; :: thesis: contradiction
then ex y being set st [y, the Element of proj2 X] in X by RELAT_1:def 5;
hence contradiction by A1; :: thesis: verum