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

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