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