 Note that actually the point \(w\) does not matter in the truth-condition for \(\mathtt{@_a\phi}\) since the satisfaction operator \(\mathtt{@_a}\) moves the point of evaluation to the reference of \(\mathtt{a}\) whatever \(w\) is.