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

{A} is a_partition of A by EQREL_1:39;

then {A} in PARTITIONS A by PARTIT1:def 3;

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

S is Classification of A

{A} is a_partition of A by EQREL_1:39;

then {A} in PARTITIONS A by PARTIT1:def 3;

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

S is Classification of A

proof

hence
{{A}} is Classification of A
; :: thesis: verum
let X be a_partition of A; :: according to TAXONOM1:def 1 :: thesis: for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds

Y is_finer_than X

thus for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds

Y is_finer_than X by Lm1; :: thesis: verum

end;Y is_finer_than X

thus for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds

Y is_finer_than X by Lm1; :: thesis: verum