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 ;

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

{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

then reconsider A19 = A1 as non negative Real ;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;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

now :: thesis: for x being object st x in X holds

[x,x] in low_toler (f,A1)

then
low_toler (f,A19) is_reflexive_in X
by RELAT_2:def 1;[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;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

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