let X be non empty finite Subset of REAL ; :: thesis: for f being Function of [:X,X:],REAL st f is symmetric & f is nonnegative holds
{X} in fam_class f
let f be Function of [:X,X:],REAL ; :: thesis: ( f is symmetric & f is nonnegative implies {X} in fam_class f )
assume A1: ( f is symmetric & f is nonnegative ) ; :: thesis: {X} in fam_class f
dom f = [:X,X:] by FUNCT_2:def 1;
then reconsider rn = rng f as non empty finite Subset of REAL by RELAT_1:65;
reconsider A1 = max rn as real number ;

now

consider x being Element of X;
assume A2: A1 is negative ; :: thesis: contradiction
f . x,x <= A1 by Th26;
hence contradiction by A1, A2, Def4; :: thesis: verum

end;

then reconsider A19 = A1 as non negative real number ;

now

let x be set ; :: thesis: ( x in X implies [x,x] in low_toler f,A1 )
assume x in X ; :: thesis: [x,x] in low_toler f,A1
then reconsider x1 = x as Element of X ;
f . x1,x1 <= A1 by Th26;
hence [x,x] in low_toler f,A1 by Def3; :: thesis: verum

end;

then low_toler f,A19 is_reflexive_in X by RELAT_2:def 1;
then reconsider R = (low_toler f,A19) [*] as Equivalence_Relation of X by A1, Th22;
Class R in fam_class f by Def5;
hence {X} in fam_class f by Th27; :: thesis: verum