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

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