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

S is Strong_Classification of A

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

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

A2: SmallestPartition A in S by A1, TARSKI:def 2;

( S is Classification of A & {A} in S ) by A1, Th14, TARSKI:def 2;

hence S is Strong_Classification of A by A2, Def2; :: thesis: verum

S is Strong_Classification of A

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

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

A2: SmallestPartition A in S by A1, TARSKI:def 2;

( S is Classification of A & {A} in S ) by A1, Th14, TARSKI:def 2;

hence S is Strong_Classification of A by A2, Def2; :: thesis: verum