let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL
for a being non negative Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds
fam_class f is non empty set
let f be PartFunc of [:X,X:],REAL; :: thesis: for a being non negative Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds
fam_class f is non empty set
let a be non negative Real; :: thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies fam_class f is non empty set )
assume ( low_toler (f,a) is_reflexive_in X & f is symmetric ) ; :: thesis: fam_class f is non empty set
then reconsider R = (low_toler (f,a)) [*] as Equivalence_Relation of X by Th22;
reconsider x = Class R as set ;
x in fam_class f by Def5;
hence fam_class f is non empty set ; :: thesis: verum