let x be set ; :: according to WAYBEL18:def 1 :: thesis: ( x in rng (I --> T) implies x is TopStruct )
assume A1: x in rng (I --> T) ; :: thesis: x is TopStruct
thus x is TopStruct by A1, TARSKI:def 1; :: thesis: verum