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