intro p hp
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → inst✝.toStruc ⊧ f
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
⊢ inst✝.toStruc ⊧ p