---

Step * of Lemma q-max-exists

∀as:ℚ List. ∃a:ℚ. ((a ∈ as) supposing ¬↑null(as) ∧ (∀a'∈as.a' ≤ a))
BY
{ xxx(xxxAutoxxx THEN D 1 THEN Reduce 0)xxx }

1
∃a:ℚ. ((a ∈ []) supposing ¬True ∧ (∀a'∈[].a' ≤ a))

2
1. u : ℚ
2. v : ℚ List
⊢ ∃a:ℚ. ((a ∈ [u / v]) supposing ¬False ∧ (∀a'∈[u / v].a' ≤ a))

---

Latex:

---

Latex:
\mforall{}as:\mBbbQ{}  List.  \mexists{}a:\mBbbQ{}.  ((a  \mmember{}  as)  supposing  \mneg{}\muparrow{}null(as)  \mwedge{}  (\mforall{}a'\mmember{}as.a'  \mleq{}  a))


By

---

Latex:
xxx(xxxAutoxxx  THEN  D  1  THEN  Reduce  0)xxx

---

Home Index