:: deftheorem Def16 defines pcs-tol-reflexive-yielding PCS_0:def 16 :
for R being Relation holds
( R is pcs-tol-reflexive-yielding iff for S being TolStr st S in rng R holds
S is pcs-tol-reflexive );