English
If there exists a chain t that contains s as a subchain and t is a superchain of s, then the successor chain of s is itself a superchain of s.
Русский
Если существует цепь t, содержащая s как подп цепь и являющаяся надцепью по отношению к s, то SuccChain r s сама является надцепью по отношению к s.
LaTeX
$$$\\\\forall \\\\alpha \\\\ r \\\\ s, \\\\(\\\\exists t, IsChain \\\\ r \\\\ s \\\\ ∧ SuperChain \\\\ r \\\\ s \\\\ t\\\\) \\\\rightarrow SuperChain \\\\ r \\\\ s \\\\ (SuccChain \\\\ r \\\\ s) $$$
Lean4
theorem succChain_spec (h : ∃ t, IsChain r s ∧ SuperChain r s t) : SuperChain r s (SuccChain r s) :=
by
have : IsChain r s ∧ SuperChain r s h.choose := h.choose_spec
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2
