I think the net formulation is quite useful to know, at least. Analysts seem to be most fond of it, as they naturally work with sequences anyway. E.g. on easily shows that the closure of a subgroup $H$ in a topological group $G$ is a subgroup: just note that for $x,y$ in closure of $H$, we find nets (wlog with the same index set) $(x_i), (y_i)$ from $H$ that converge to $x$, resp. $y$, and then $x_i \cdot {y_i}^{-1} \rightarrow x \cdot y^{-1}$ from continuity of the group operations, and the left hand side lives in $H$, so the right hand side is in closure H, and this is thus a subgroup.

Similarly, $A \cdot B$ is closed in $G$ when $A$ is closed and $B$ is compact: take a net $(x_i \cdot y_i)_{i \in I}$ in $A \cdot B$ converging to $z$. By compactness the net $(y_i)$ has a subnet converging to $y \in B$, indexed by $J$ say, and then the corresponding subnet $x_j = x_j \cdot y_j \cdot y_j^{-1}$ converges to $z \cdot y^{-1}$ and as the $(x_j)$ are in $A$, so is the limit $z \cdot y^{-1}$ and so $z = (z \cdot y^{-1} \cdot y)$ is in $A \cdot B$, making it closed.

Nets also make for a nice formulation of the Riemann integral (using partitions on the interval as a directed set under refinement) as a limit of a certain net. Some proofs just look more "natural" in a net formulation, I think. One can do the proof for sequences first, and see how it generalizes using nets.

1more comment