theorem :: TAXONOM1:29

for X being non empty set
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