let F be Relation; :: thesis: ( F is TopSpace-yielding implies F is TopStruct-yielding )
assume F is TopSpace-yielding ; :: thesis: F is TopStruct-yielding
then for x being object st x in rng F holds
x is TopStruct ;
hence F is TopStruct-yielding by WAYBEL18:def 1; :: thesis: verum