No that would not be okay. We need to explain why A[c WU b] does not hold on all initial states, i.e., on state s3 and s6. We can explain that it does hold on s6 as follows: A[c WU b] is equivalent to b | c &AX A[c WU b], and since s6 satisfies b, it also satisfies A[c WU b].
However, it does not hold on s3, since on s3, we have c, but not b, so that we have to check that all successor states of s3, i.e., s5 satisfies A[c WU b]. This is however not the case, since s5 is neither labeled with b nor with c.
