let X be set ; :: thesis: ( ( for x, y being object holds not [x,y] in X ) implies ( proj1 X = {} & proj2 X = {} ) )
set x = the Element of proj2 X;
assume A1: for x, y being object 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 object st [ the Element of proj1 X,y] in X by XTUPLE_0:def 12;
hence contradiction by A1; :: thesis: verum
end;
assume proj2 X <> {} ; :: thesis: contradiction
then ex y being object st [y, the Element of proj2 X] in X by XTUPLE_0:def 13;
hence contradiction by A1; :: thesis: verum