assume not proj1 X is empty ; :: thesis: contradiction
then consider x being set such that
W: x in proj1 X by XBOOLE_0:def 1;
ex y being set st [x,y] in X by W, Def4;
hence contradiction ; :: thesis: verum