:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def 17 :
for F being Relation holds
( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds
not S is trivial );