have : System.Inconsistent (insert (~σ) T) := this.of_supset ssu
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁴ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝² : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝¹ : ¬Satisfiable ↑u'
this✝ : System.Inconsistent ↑u'
this : System.Inconsistent ↑u
⊢ T ⊢! σ
case intro
L : Language
T : Theory L
σ : Sentence L
h : T ⊨ σ
this✝⁵ : (α : Type u) → DecidableEq α := Classical.typeDecidableEq
u : Finset (Sentence L)
ssu : ↑u ⊆ insert (~σ) T
hu : ¬Satisfiable ↑u
this✝⁴ : (k : ℕ) → Encodable ((languageFinset u).Func k)
this✝³ : (k : ℕ) → Encodable ((languageFinset u).Rel k)
u' : Finset (Sentence (languageFinset u)) := u.imageOfFinset fun x hσ => toSubLanguageFinsetSelf hσ
image_u' : Finset.image (⇑(lMap L.ofSubLanguage)) u' = u
this✝² : ¬Satisfiable ↑u'
this✝¹ : System.Inconsistent ↑u'
this✝ : System.Inconsistent ↑u
this : System.Inconsistent (insert (~σ) T)
⊢ T ⊢! σ