let X be set ; :: thesis: ( ( for x, y being set holds not [x,y] in X ) implies ( proj1 X = {} & proj2 X = {} ) )
consider x being 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 = {}

consider x being Element of proj1 X;
assume proj1 X <> {} ; :: thesis: contradiction
then ex y being set st [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,x] in X by RELAT_1:def 5;
hence contradiction by A1; :: thesis: verum