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
then dom (X --> N) <> {} by RELAT_1:65;
then X <> {} ;
then rng (X --> N) = {N} by FUNCOP_1:14;
hence i is net of T by A1, TARSKI:def 1; :: thesis: verum