:: deftheorem Def1 defines Group-yielding GROUP_23:def 1 :
for IT being Relation holds
( IT is Group-yielding iff for G being object st G in rng IT holds
G is Group );