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