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