Solution (source code)

= Solution

The <transitive closure> $\operatorname{TC}(a)$ is the least <transitive set> containing $a$ as a subset. Put $a_0=a$, $a_{n+1}=\bigcup a_n$ and define
$$
\boxed{\operatorname{TC}(a)=\bigcup_{n<\omega}a_n.}
$$
Recursion and <Replacement> give the set of iterates, and Union gives its union. It contains $a=a_0$ as a subset. If $u\in v\in\operatorname{TC}(a)$, then $v\in a_n$ for some $n$, so $u\in a_{n+1}\subseteq\operatorname{TC}(a)$; hence it is transitive.

If $T$ is transitive with $a\subseteq T$, induction gives $a_n\subseteq T$ for every $n$, because $\bigcup T\subseteq T$. Therefore $\operatorname{TC}(a)\subseteq T$. This proves minimality and uniqueness. If the alternative convention asks for the least <transitive set> containing $a$ as an element, that set is $\operatorname{TC}(\{a\})$.