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