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