set LH = proj1 [:X,Y:];
(proj1 [:X,Y:]) \ X = {} ;
then reconsider LH = proj1 [:X,Y:] as Subset of X by Th29;
LH /\ X = LH null X ;
hence ((proj1 [:X,Y:]) /\ X) \+\ (proj1 [:X,Y:]) is empty ; :: thesis: verum