consider R being non empty TopSpace;
take J = I --> R; :: thesis: ( J is TopSpace-yielding & J is non-Empty )
thus J is TopSpace-yielding :: thesis: J is non-Empty

proof

let x be set ; :: according to WAYBEL18:def 1 :: thesis: ( x in rng J implies x is TopStruct )
assume x in rng J ; :: thesis: x is TopStruct
hence x is TopStruct by TARSKI:def 1; :: thesis: verum

end;

thus J is non-Empty :: thesis: verum

proof

let S be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not S in proj2 J or not S is empty )
assume S in rng J ; :: thesis: not S is empty
hence not S is empty by TARSKI:def 1; :: thesis: verum

end;