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

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