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