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