intro ⟨hyx, hxy⟩
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
⊢ ¬(r y x ∧ r x y)
α : Sort u_1
r : α → α → Prop
self : PartialOrder r
inst✝ : WeaklyComplementedRel r
x y : α
hne : x ≠ y
hyx : r y x
hxy : r x y
⊢ False