set R = the TopStruct ;
take I --> the TopStruct ; :: thesis: I --> the TopStruct is TopStruct-yielding
let v be set ; :: according to PENCIL_1:def 13 :: thesis: ( v in rng (I --> the TopStruct ) implies v is TopStruct )
assume A1: v in rng (I --> the TopStruct ) ; :: thesis: v is TopStruct
rng (I --> the TopStruct ) c= { the TopStruct } by FUNCOP_1:13;
hence v is TopStruct by A1, TARSKI:def 1; :: thesis: verum