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

proof

let x be object ; :: 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 rng 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;