[STATEMENT]
theorem main: \<open>(\<turnstile> p) = (\<forall>I. I \<Turnstile> p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<turnstile> p) = (\<forall>I. I \<Turnstile> p)
[PROOF STEP]
using soundness completeness
[PROOF STATE]
proof (prove)
using this:
\<turnstile> ?p \<Longrightarrow> ?I \<Turnstile> ?p
\<forall>I. I \<Turnstile> ?p \<Longrightarrow> \<turnstile> ?p

goal (1 subgoal):
 1. (\<turnstile> p) = (\<forall>I. I \<Turnstile> p)
[PROOF STEP]
by blast