I'm reading the book 'The lambda calculus its syntax and semantics'. In part 5, chapter 19: Local structure of Models, more specifically 19.2 Local structure of $D_\infty$, the notation $D_\infty \vDash M \sqsubseteq N$ is used. This relation is used to proof that the theory of $D_\infty$ corresponds with the theory of $K^*$.

My question is that anyones knows where it stands for. I can't find the symbol in the index of symbols. I didn't came across the symbol (except when dealing in cpo's) in the context of terms. I can't figure out the meaning/definition it by reading the proofs.

The proofs where it is used, aren't fully worked out since it looks like that of the local structure of $P\omega$. But there the notation $\subseteq$ is used instead of $\sqsubseteq$. As $P\omega$ is is ordered by inclusion and $D_\infty$ is a CPO (ordered by $\sqsubseteq$), I would think that the notation comes from there, but then I don't see how a model derives the 'inclusion' since models (and theories) only deal with equality of terms (under their evaluation).