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