proj1 [:X,U:] = X by FUNCT_5:9;
hence (proj1 [:X,U:]) \+\ X is empty ; :: thesis: verum