---

Step * of Lemma qv-convex-and

∀[S1,S2:(ℚ List) ⟶ ℙ].  (qv-convex(p.S1[p]) ⇒ qv-convex(p.S2[p]) ⇒ qv-convex(p.S1[p] ∧ S2[p]))
BY
{ (Auto THEN All (Unfold `qv-convex`) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[S1,S2:(\mBbbQ{}  List)  {}\mrightarrow{}  \mBbbP{}].    (qv-convex(p.S1[p])  {}\mRightarrow{}  qv-convex(p.S2[p])  {}\mRightarrow{}  qv-convex(p.S1[p]  \mwedge{}  S2[p]))


By

---

Latex:
(Auto  THEN  All  (Unfold  `qv-convex`)  THEN  Auto)

---

Home Index