:: deftheorem defines TolStr-yielding PCS_0:def 13 :
for R being Relation holds
( R is TolStr-yielding iff for P being set st P in rng R holds
P is TolStr );