---

Step * of Lemma Veldman-Ramsey

∀T:Type. ∀n:ℕ.  ∀[R,S:n-aryRel(T)].  (almost-full(T;n;R) ⇒ almost-full(T;n;S) ⇒ almost-full(T;n;R ∧ S))
BY
{ (Auto THEN D -2 THEN D -1) }

1
1. T : Type@i'
2. n : ℕ@i
3. [R] : n-aryRel(T)
4. [S] : n-aryRel(T)
5. p : wfd-tree(T)@i
6. tree-secures(T;[[R]];p)@i
7. p1 : wfd-tree(T)@i
8. tree-secures(T;[[S]];p1)@i
⊢ almost-full(T;n;R ∧ S)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}n:\mBbbN{}.
    \mforall{}[R,S:n-aryRel(T)].    (almost-full(T;n;R)  {}\mRightarrow{}  almost-full(T;n;S)  {}\mRightarrow{}  almost-full(T;n;R  \mwedge{}  S))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1)

---

Home Index