---

Step * of Lemma qmax-list-member

∀L:ℚ List. (qmax-list(L) ∈ L) supposing 0 < ||L||
BY
{ xxx(Auto
      THEN Unfold `qmax-list` 0
      THEN BLemma `combine-list-member`
      THEN Auto
      THEN Unfold `qmax` 0
      THEN AutoSplit
      THEN Auto
      THEN TrivialOr)xxx }

---

Latex:

---

Latex:
\mforall{}L:\mBbbQ{}  List.  (qmax-list(L)  \mmember{}  L)  supposing  0  <  ||L||


By

---

Latex:
xxx(Auto
        THEN  Unfold  `qmax-list`  0
        THEN  BLemma  `combine-list-member`
        THEN  Auto
        THEN  Unfold  `qmax`  0
        THEN  AutoSplit
        THEN  Auto
        THEN  TrivialOr)xxx

---

Home Index