PA in PARTITIONS Y by PARTIT1:def 3;
hence {PA} is Subset of (PARTITIONS Y) by ZFMISC_1:31; :: thesis: verum