\begin{definition}[Definition:Labeled Tree for Propositional Logic/Child WFF]
Let $\left({T, \mathbf H, \Phi}\right)$ be a labeled tree for propositional logic.
A WFF that is attached to a child of a node $t$ is called a '''child WFF of $t$'''.
\end{definition}