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
not fam_class f is empty
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
not fam_class f is empty
let a be non negative Real; :: thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies not fam_class f is empty )
assume ( low_toler (f,a) is_reflexive_in X & f is symmetric ) ; :: thesis: not fam_class f is empty
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 not fam_class f is empty ; :: thesis: verum