existsi Ω
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ Ω₂ ≺^[t.m] Ω ∧ Ω₃ ≺^[t.n] Ω