:: deftheorem Def1 defines TopStruct-yielding WAYBEL18:def 1 :
for F being Relation holds
( F is TopStruct-yielding iff for x being object st x in rng F holds
x is TopStruct );