---

Step * of Lemma order-type-less-maximal

∀x:WFTRO{i:l}(). (x order-type-less() max-WO{i:l}())
BY
{ xxx(Unfold `max-WO` 0 THEN Auto)xxx }

1
1. x : WFTRO{i:l}()
⊢ x order-type-less() <WFO{i:l}(), order-type-less(), DCC-order-type()>

---

Latex:

---

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


By

---

Latex:
xxx(Unfold  `max-WO`  0  THEN  Auto)xxx

---

Home Index