---

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

Trans(WFO{i:l}();x,y.order-type-less() x y)
BY
{ xxxExtract of Obid: order-type-less-transitive
     not unfolding  compose
     finishing with (RepUR ``compose ot-less-trans`` 0 THEN Auto)
     normalizes to:
     
     ot-less-trans()xxx }

---

Latex:

---

Latex:
Trans(WFO\{i:l\}();x,y.order-type-less()  x  y)


By

---

Latex:
xxxExtract  of  Obid:  order-type-less-transitive
      not  unfolding    compose
      finishing  with  (RepUR  ``compose  ot-less-trans``  0  THEN  Auto)
      normalizes  to:
     
      ot-less-trans()xxx

---

Home Index