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 i in rng (X --> N) ; :: thesis: i is net of T
hence i is net of T by TARSKI:def 1; :: thesis: verum