An implication p->q is just an abbreviation for !p|q, so that we can use the rules for the latter. However, there were brackets missing in the example solution that I have now added, maybe that was confusing for you. Please check again!

The same answer could be given for global model checking. Hence, States(p->q) = States(!p|q) = States(!p)âˆªStates(q) = (S\States(p))âˆªStates(q).