:: deftheorem Def9 defines AbGroup-yielding PRVECT_1:def 10 :
for F being Relation holds
( F is AbGroup-yielding iff for x being set st x in rng F holds
x is AbGroup );