theorem
LO.Modal.Standard.Kripke.reducible_of_subset_FrameClass
{α : Type u_1}
{Ax₁ : LO.Modal.Standard.AxiomSet α}
{Ax₂ : LO.Modal.Standard.AxiomSet α}
(𝔽₁ : LO.Kripke.FrameClass)
(𝔽₂ : LO.Kripke.FrameClass)
[sound₁ : LO.Sound (𝝂Ax₁) 𝔽₁#α]
[complete₂ : LO.Complete (𝝂Ax₂) 𝔽₂#α]
(h𝔽 : 𝔽₂ ⊆ 𝔽₁)
:
theorem
LO.Modal.Standard.Kripke.equiv_of_eq_FrameClass
{α : Type u_1}
{Ax₁ : LO.Modal.Standard.AxiomSet α}
{Ax₂ : LO.Modal.Standard.AxiomSet α}
(𝔽₁ : LO.Kripke.FrameClass)
(𝔽₂ : LO.Kripke.FrameClass)
[sound₁ : LO.Sound (𝝂Ax₁) 𝔽₁#α]
[sound₂ : LO.Sound (𝝂Ax₂) 𝔽₂#α]
[complete₁ : LO.Complete (𝝂Ax₁) 𝔽₁#α]
[complete₂ : LO.Complete (𝝂Ax₂) 𝔽₂#α]
(h𝔽 : 𝔽₁ = 𝔽₂)
: