consider T being TopSpace;
take I --> T ; :: thesis: I --> T is TopSpace-yielding
let v be set ; :: according to WAYBEL18:def 1 :: thesis: ( v in rng (I --> T) implies v is TopStruct )
A1: rng (I --> T) c= {T} by FUNCOP_1:19;
assume v in rng (I --> T) ; :: thesis: v is TopStruct
hence v is TopStruct by A1, TARSKI:def 1; :: thesis: verum