let X be non empty finite Subset of REAL; :: thesis: for f being Function of [:X,X:],REAL st SmallestPartition X in fam_class f & f is symmetric & f is nonnegative holds
fam_class f is Strong_Classification of X
let f be Function of [:X,X:],REAL; :: thesis: ( SmallestPartition X in fam_class f & f is symmetric & f is nonnegative implies fam_class f is Strong_Classification of X )
assume that
A1: SmallestPartition X in fam_class f and
A2: ( f is symmetric & f is nonnegative ) ; :: thesis: fam_class f is Strong_Classification of X
A3: fam_class f is Classification of X by Th31;
{X} in fam_class f by A2, Th30;
hence fam_class f is Strong_Classification of X by A1, A3, Def2; :: thesis: verum