---

Step * of Lemma DCC-order-type_wf

DCC-order-type() ∈ DCC(WFO{i:l}();order-type-less())
BY
{ xxx(Assert TERMOF{DCC-order-type-less-ext:o, \\v:l, i:l} ∈ DCC(WFO{i:l}();order-type-less()) BY
            Auto)xxx }

1
1. TERMOF{DCC-order-type-less-ext:o, \\v:l, i:l} ∈ DCC(WFO{i:l}();order-type-less())
⊢ DCC-order-type() ∈ DCC(WFO{i:l}();order-type-less())

---

Latex:

---

Latex:
DCC-order-type()  \mmember{}  DCC(WFO\{i:l\}();order-type-less())


By

---

Latex:
xxx(Assert  TERMOF\{DCC-order-type-less-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  \mmember{}  DCC(WFO\{i:l\}();order-type-less())  BY
                    Auto)xxx

---

Home Index