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;