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