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