:: deftheorem defines non-void-yielding PENCIL_1:def 15 :
for F being TopStruct-yielding Function holds
( F is non-void-yielding iff for i being set st i in rng F holds
i is non void TopStruct );