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