---

Step * of Lemma order-type-less-maximal-ext

∀x:WFTRO{i:l}(). (x order-type-less() max-WO{i:l}())
BY
{ Extract of Obid: order-type-less-maximal
  normalizes to:
  
  Maximal_order_type()
  finishing with (Fold `Maximal_order_type` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:WFTRO\{i:l\}().  (x  order-type-less()  max-WO\{i:l\}())


By

---

Latex:
Extract  of  Obid:  order-type-less-maximal
normalizes  to:

Maximal\_order\_type()
finishing  with  (Fold  `Maximal\_order\_type`  0  THEN  Auto)

---

Home Index