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)