Ax. 1.{P(φ)∧□∀x[φ(x)→ψ(x)]}→P(ψ)
Ax. 2.P(¬φ)↔¬P(φ)
Th. 1.P(φ)→◊∃x[φ(x)]
Df.1.G(x)⟺∀φ[P(φ)→φ(x)]
Ax. 3.P(G)
Th. 2.◊∃xG(x)
Df. 2.φ ess x⟺φ(x)∧∀ψ{ψ(x)→□∀y[φ(y)→ψ(y)]}
Ax. 4.P(φ)→□P(φ)
Th. 3.G(x)→G ess x
Df. 3.E(x)⟺∀φ[φ ess x→□∃yφ(y)]
Ax. 5.P(E)
Th. 4.□∃xG(x)