{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

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