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

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