# Can someone clarify Invariant 4.7 of the PBFT correctness proof paper?

I am reading the PBFT Correctness Proof Paper and I cannot make completely sense of the Invariant 4.7 and its proof:

Here are my concerns:

1. I assume that the symbol $\Leftrightarrow$ is used with the usual meaning of double implication.
2. $n\mbox{-}faulty$ is defined (Definition 4.3) as the number of faulty replicas, so I do not understand how it can be used as a predicate in Invariant 4.7.
When is $n\mbox{-}faulty$ true of false?