contrapose
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ F ⊧* 𝗟 → Transitive F.Rel
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
⊢ ¬Transitive F.Rel → ¬F ⊧* 𝗟