---

Step * of Lemma ocmon_connex

∀g:OCMon. ∀x,y:|g|.  ((↑(x ≤b y)) ∨ (↑(y ≤b x)))
BY
{ ((ProvePropertyLemma `connex` 1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}x,y:|g|.    ((\muparrow{}(x  \mleq{}\msubb{}  y))  \mvee{}  (\muparrow{}(y  \mleq{}\msubb{}  x)))


By

---

Latex:
((ProvePropertyLemma  `connex`  1)  THEN  Auto)

---

Home Index