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