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:42;
reconsider A1 = max rn as Real ;
now :: thesis: not A1 is negative
set x = the Element of X;
assume A2: A1 is negative ; :: thesis: contradiction
f . ( the Element of X, the Element of X) <= A1 by Th26;
hence contradiction by A1, A2; :: thesis: verum
end;
then reconsider A19 = A1 as non negative Real ;
now :: thesis: for x being object st x in X holds
[x,x] in low_toler (f,A1)
let x be object ; :: 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