:: deftheorem Def16 defines trivial-yielding PENCIL_1:def 16 :
for F being Relation holds
( F is trivial-yielding iff for S being set st S in rng F holds
S is trivial );