:: deftheorem DefAA defines non-empty-addLoopStr-yielding PRVECT_1:def 9 :
for F being Relation holds
( F is non-empty-addLoopStr-yielding iff for x being set st x in rng F holds
x is non empty addLoopStr );