How to prove a LTL formula correct in a specific model?

Question

I have been learning Verification by model checking recently and I get the following question:

$Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ or\ not\ in\ this\ model\ M?$

And there is the description of the model. .

I think it is correct, because the next state of $q_3$ is $q_1$ or $q_2$ and the next state of $q_1$ is $q_2$. So I get an infinite loop about $q_2$, which satisfies $F\ G\ \lnot a$. But I only can give the thought of my prove in natural language not mathematical rigor way.

if not mind, could anyone tell me my thought is right or wrong and prove it in a mathematical rigor way?

Thanks in advances