---

Step * of Lemma max_w_ord_wf

∀[T:Type]. ∀[t1,t2:T]. ∀[f:T ─→ ℤ].  (max_w_ord(t1;t2;f) ∈ T)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[T:Type].  \mforall{}[t1,t2:T].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (max\_w\_ord(t1;t2;f)  \mmember{}  T)


By

ProveWfLemma

---

Home Index