:: deftheorem Def4 defines transitive-yielding PCS_0:def 4 :
for R being Relation holds
( R is transitive-yielding iff for S being RelStr st S in rng R holds
S is transitive );