let A be non empty set ; :: thesis: for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds

S is Classification of A

let S be Subset of (PARTITIONS A); :: thesis: ( S = {{A},(SmallestPartition A)} implies S is Classification of A )

assume A1: S = {{A},(SmallestPartition A)} ; :: thesis: S is Classification of A

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

A2: X in S and

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

S is Classification of A

let S be Subset of (PARTITIONS A); :: thesis: ( S = {{A},(SmallestPartition A)} implies S is Classification of A )

assume A1: S = {{A},(SmallestPartition A)} ; :: thesis: S is Classification of A

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

A2: X in S and

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

per cases
( X = {A} or X = SmallestPartition A )
by A1, A2, TARSKI:def 2;

end;

suppose A4:
X = {A}
; :: thesis: ( X is_finer_than Y or Y is_finer_than X )

end;

per cases
( Y = {A} or Y = SmallestPartition A )
by A1, A3, TARSKI:def 2;

end;

suppose A5:
X = SmallestPartition A
; :: thesis: ( X is_finer_than Y or Y is_finer_than X )

end;

per cases
( Y = SmallestPartition A or Y = {A} )
by A1, A3, TARSKI:def 2;

end;