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: S is Classification of A by A1, Th14;
A3: {A} in S by A1, TARSKI:def 2;
SmallestPartition A in S by A1, TARSKI:def 2;
hence S is Strong_Classification of A by A2, A3, Def2; :: thesis: verum