. apply reducible_of_subset_axiomSetFrameClass hs₂;
case right
α : Type u
inst✝² : DecidableEq α
L₁ L₂ : DeductionParameter α
inst✝¹ : L₁.HasNec
inst✝ : L₂.HasNec
P₁ P₂ : FrameProperty
sound₁ : Sound L₁ 𝔽(Ax(L₁))
sound₂ : Sound L₂ 𝔽(Ax(L₂))
complete₁ : Complete L₁ 𝔽(Ax(L₁))
complete₂ : Complete L₂ 𝔽(Ax(L₂))
definability₁ : Definability Ax(L₁) P₁
definability₂ : Definability Ax(L₂) P₂
hs₁ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₂)) → F ∈ 𝔽(Ax(L₁))
hs₂ : ∀ {F : Frame}, F ∈ 𝔽(Ax(L₁)) → F ∈ 𝔽(Ax(L₂))
⊢ L₂ ≤ₛ L₁
no goals