:: deftheorem defines non-void-yielding PENCIL_1:def 14 :
for F being Relation holds
( F is non-void-yielding iff for S being TopStruct st S in rng F holds
not S is void );