suffices p ∈ Ω.theory by exact truthlemma.mpr this;
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ Ω ⊧ p
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : L ⊢! p
Ω : (CanonicalModel L).World
⊢ p ∈ Ω.theory