let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:], REAL
for a being non negative real number 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 number 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 number ; :: thesis: ( low_toler f,a is_reflexive_in X & f is symmetric implies fam_class f is non empty set )
assume A1: ( low_toler f,a is_reflexive_in X & f is symmetric ) ; :: thesis: fam_class f is non empty set
reconsider R = (low_toler f,a) [*] as Equivalence_Relation of X by A1, Th22;
reconsider x = Class R as set ;
x in fam_class f by Def5;
hence fam_class f is non empty set ; :: thesis: verum