English
If hs is a strong antichain on s and the inequality condition holds, then IsStrongAntichain r (insert a s).
Русский
Если s является сильной антицепью и выполняется требуемое неравенство, то IsStrongAntichain r (insert a s).
LaTeX
$$$\\text{IsStrongAntichain}(r, s) \\rightarrow (\\forall b, b \\in s \\rightarrow a \\neq b \\rightarrow \\forall c, \\lnot r a c \\lor \\lnot r b c) \\rightarrow \\text{IsStrongAntichain}(r, \\operatorname{Set.instInsert.insert}(a, s))$$$
Lean4
protected theorem insert (hs : IsStrongAntichain r s) (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c) :
IsStrongAntichain r (insert a s) :=
isStrongAntichain_insert.2 ⟨hs, h⟩
