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