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