constructor
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) ↔ ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p
case mp
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p) → ∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p

case mpr
L : Language
inst✝¹¹ : L.ORing
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
T : Theory ℒₒᵣ
⊢ (∀ {p : Sentence ℒₒᵣ}, p ∈ T → M ⊧ₘ p) → ∀ {p : Sentence L}, p ∈ Theory.lMap oringEmb T → M ⊧ₘ p