simpa [Satisfies] using h w₃ r₂₃
case pos
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
w₁ w₃ : F.World
nr₁₃ : ¬F.Rel w₁ w₃
x : F.World
hx : w₁ ≺ x
r₁₂ : F.Rel w₁ x
r₂₃ : F.Rel x w₃
h : ∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } w' (atom default)
⊢ Satisfies { Frame := F, Valuation := fun w' x_1 => w' ≠ x ∧ w' ≠ w₃ } x (atom default)
no goals