exact H.of_supset h𝓕
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
left✝ : Collection.Finite 𝓕
H : Inconsistent 𝓕
⊢ Inconsistent 𝓢
no goals