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 )

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

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

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

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

hence ( X is_finer_than Y or Y is_finer_than X ) by A4; :: thesis: verum

end;

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

hence ( X is_finer_than Y or Y is_finer_than X ) by A4, Th11; :: thesis: verum

end;

end;

end;

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

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

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

hence ( X is_finer_than Y or Y is_finer_than X ) by A5; :: thesis: verum

end;

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

hence ( X is_finer_than Y or Y is_finer_than X ) by A5, Th11; :: thesis: verum

end;

end;

end;

end;