(proj1 [:X,Y:]) \+\ X = {} ;
hence proj1 [:X,Y:] = X by Th29; :: thesis: verum