consider N being net of T;
take X --> N ; :: thesis: for i being set st i in rng (X --> N) holds
i is net of T
let i be set ; :: thesis: ( i in rng (X --> N) implies i is net of T )
assume A1: i in rng (X --> N) ; :: thesis: i is net of T
thus i is net of T by A1, TARSKI:def 1; :: thesis: verum