assume not proj2 X is empty ; :: thesis: contradiction
then consider x being object such that
A1: x in proj2 X ;
ex y being object st [y,x] in X by A1, Def13;
hence contradiction ; :: thesis: verum