let A be non empty set ; :: thesis: {(SmallestPartition A)} is Classification of A

SmallestPartition A in PARTITIONS A by PARTIT1:def 3;

then reconsider S = {(SmallestPartition A)} as Subset of (PARTITIONS A) by ZFMISC_1:31;

S is Classification of A

SmallestPartition A in PARTITIONS A by PARTIT1:def 3;

then reconsider S = {(SmallestPartition A)} as Subset of (PARTITIONS A) by ZFMISC_1:31;

S is Classification of A

proof

hence
{(SmallestPartition A)} is Classification of A
; :: thesis: verum
let X, Y be a_partition of A; :: according to TAXONOM1:def 1 :: thesis: ( X in S & Y in S & not X is_finer_than Y implies Y is_finer_than X )

assume that

A1: X in S and

A2: Y in S ; :: thesis: ( X is_finer_than Y or Y is_finer_than X )

X = SmallestPartition A by A1, TARSKI:def 1;

hence ( X is_finer_than Y or Y is_finer_than X ) by A2, TARSKI:def 1; :: thesis: verum

end;assume that

A1: X in S and

A2: Y in S ; :: thesis: ( X is_finer_than Y or Y is_finer_than X )

X = SmallestPartition A by A1, TARSKI:def 1;

hence ( X is_finer_than Y or Y is_finer_than X ) by A2, TARSKI:def 1; :: thesis: verum