---

Step * of Lemma grp_lt_irreflexivity

∀[g:OCMon]. ∀[a:|g|].  False supposing a < a
BY
{ ProveSpecializedLemma `set_lt_irreflexivity` 1 [parm{i};g↓oset] 
   (AbReduceC ANDTHENC FoldsC ``grp_lt``) }

---

Latex:

---

Latex:
\mforall{}[g:OCMon].  \mforall{}[a:|g|].    False  supposing  a  <  a


By

---

Latex:
ProveSpecializedLemma  `set\_lt\_irreflexivity`  1  [parm\{i\};g\mdownarrow{}oset] 
      (AbReduceC  ANDTHENC  FoldsC  ``grp\_lt``)

---

Home Index