:: deftheorem Def5 defines Poset-yielding YELLOW16:def 5 :
for R being Relation holds
( R is Poset-yielding iff for x being set st x in rng R holds
x is Poset );