Concept used in the proof
An unquantified CNF formula consisting of clauses containing a single positive literal plus any number of negated literals is always satisfiable.  To produce a satisfying assignment, you simply set all the positive literals to true, satisfying all the clauses.  If you existentially quantify the variables associated with the positive literals and allow arbitrary quantification of the remaining variables, the formula is still satisfiable, and  for the same reason.  In the proof of the theorem, $P_\mathit{\Phi}$ is the subset of such clauses from the Horn formula $\mathit{\Phi}$.  Thus $P_\mathit{\Phi}$ by itself is always satisfiable.  It follows that $\mathit{\Phi}$ can only be unsatisfiable if, out of the sets of remaining clauses (denoted $N^+_\mathit{\Phi}$ and $N_\mathit{\Phi}$), a clause requires one of the previously set positive literals in $P_\mathit{\Phi}$ to be set false and there is no other way to satisfy the previously satisfied clause.