set T = the TopSpace;
take I --> the TopSpace ; :: thesis: I --> the TopSpace is TopStruct-yielding
let v be set ; :: according to WAYBEL18:def 1 :: thesis: ( v in rng (I --> the TopSpace) implies v is TopStruct )
assume v in rng (I --> the TopSpace) ; :: thesis: v is TopStruct
hence v is TopStruct by TARSKI:def 1; :: thesis: verum