Understanding pre\image inclusion manipulations For $f: (X, \tau) \to (Y, \tau'), \ f^{-1}(\tau' \text{ closed } K \subseteq Y)$ is $\tau$ closed in $X \implies f(\overline {A}) \subseteq \overline{f(A)}$ for all $A \subseteq X.$
Proof:

Suppose $f^{–1}(\text{each $\tau′$- closed set})$ is $\tau$-closed.


Given $A \subseteq X: \overline{f(A)} \text{ is } \tau′$-closed,


therefore $f^{–1}(\overline{f(A)}) \text{ is } \tau$-closed.


But $A \subseteq f^{–1}(f (A)) \subseteq f^{–1}(\overline{f(A)})$,


therefore $\overline A \subseteq f^{–1}(\overline{f(A)})$,


that is, $f(\overline{A}) \subseteq \overline{f(A)}$.

I'd like to check my understanding of this proof line by line(each line corresponds to a separate quote). Want to become more fluent in set inclusion manipulations for pre\images. I feel there's some underlying complexity wrt to this topic which is not elaborated on enough. For example, $f(x) \in f(A)$ implies $(1) \ x \in f^{-1}(f(A))$ or $(2) \ x \in A$ if $f$ is injective or $(3) \ \exists x \in A$ s.t. $f(x) \in f(A)$.
So,
Second line: $\overline{f(A)}$ is a closure and every closure is closed.
Third line: it's by assumption.
Fourth line: $x \in A \implies f(x) \in f(A) \implies f(x) \in \overline{f(A)}$ by def of closure $\implies x \in f^{-1}(\overline{f(A)})$.
Fifth line: the fourth line above implies $\overline A \subseteq f^{-1}\overline{(f(\overline{A}))}$, so how did they get their conclusion in the fifth line? One possibility is that $A$ is closed in which case $A = \overline A$, but how do we know that?
Sixth line: $y \in f(\overline{A}) \implies \exists x \in \overline{A}$ s.t. $f(x) = y$ by definition of image set $\implies x \in  f^{-1}(\overline{f(A)})$ as $\overline{A} \subseteq f^{-1}(\overline{f(A)}) \implies f(x) \in \overline{f(A)}$.
My questions:
Is my understanding correct? How did they get the fifth line? Thanks.
 A: My recap with comments:
Suppose that $f$ is continuous, i.e. for every closed subset $C$ of $(Y, \tau')$ we have $f^{-1}[C]$ closed in $(X,\tau)$.
We want to show that $f[\overline{A}] \subseteq \overline{f[A]}$ for all $A \subseteq X$.
So let $A \subseteq X$ be arbitrary.
Then $\overline{f[A]}$ is closed in $(Y, \tau')$ as all closures of sets are closed.
So by continuity, $f^{-1}[\overline{f[A]}]$ is closed in $(X,\tau)$.
$A \subseteq f^{-1}[f[A]]$ is by true by the definitions: if $x \in A$ then $f(x) \in f[A]$ by definition of $f[A]$ and so $x \in f^{-1}[f[A]]$ by definition of the inverse image ($x \in f^{-1}[B]$ iff $f(x) \in B$, applied to $B=f[A]$). Another general fact is: $B \subseteq C$ implies $f^{-1}[B] \subseteq f^{-1}[C]$ and also $f[B] \subseteq f[C]$, these are easily seen by applying the definitions (and should be well-known to any student of maths). Applying this to $B= f[A]$ and $C= \overline{f[A]}$ (where $B \subseteq C$ is clear) gives the final inclusion in
$$A \subseteq f^{-1}[f[A]] \subseteq f^{-1}[\overline{f[A]}]\tag{1}$$
So we have now that $A$ is a subset of a closed subset $f^{-1}[\overline{f[A]}]$ and so $$\overline{A} \subseteq f^{-1}[\overline{f[A]}]\tag{2}$$ as well (either apply closure on both sides of $(1)$, applying $B \subseteq C \to \overline{B}\subseteq \overline{C}$ and $\overline{C}=C$ for closed $C$; or the fact that the closure of $A$ is the minimal closed superset of $A$).
The final conclusion $$f[\overline{A}] \subseteq \overline{f[A]}$$ follows from $(2)$ by definitions: $y \in f[\overline{A}]$ means $y= f(x)$ for some $x \in \overline{A}$, $(2)$ then says that $x \in f^{-1}[\overline{f[A]}]$ so by definition of $f^{-1}$, $y = f(x) \in \overline{f[A]}$, as required.
This mostly seems to follow your comments as well.
