{A} is a_partition of A by EQREL_1:39;
then A1: {A} in PARTITIONS A by PARTIT1:def 3;
SmallestPartition A in PARTITIONS A by PARTIT1:def 3;
then reconsider S = {{A},(SmallestPartition A)} as Subset of (PARTITIONS A) by A1, ZFMISC_1:32;
take S ; :: thesis: ( S is Classification of A & {A} in S & SmallestPartition A in S )
thus ( S is Classification of A & {A} in S & SmallestPartition A in S ) by Th14, TARSKI:def 2; :: thesis: verum