 Assume that \(F \vdash \neg G_F\). Then \(F\) cannot prove \(G_F\), for otherwise \(F\) would be simply inconsistent. Hence no natural number \(\boldsymbol{n}\) is the Gödel number of a proof of \(G_F\), and because the proof relation is strongly representable, for all \(\boldsymbol{n}\), \(F \vdash \neg\Prf_F (\underline{n}, \ulcorner G_F\urcorner)\).  If also \(F \vdash \exists x\Prf_F (x, \ulcorner G_F\urcorner)\), \(F\) is not 1-consistent, against the assumption. Therefore \(F\) does not prove \(\exists x\Prf_F (x, \ulcorner G_F\urcorner)\), in other words, by the definition of \(\Prov_F (x), F\) does not prove \(\Prov_F (\ulcorner G_F\urcorner)\).  By the key equivalence (G), \(F\) also does not prove \(\neg G_F\).