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