---

Step * 1 of Lemma ocmon_trans

.....assertion..... 
∀[g:OCMon]. ∀[a,b,c:|g|].  ((↑(a ≤b b)) ⇒ (↑(b ≤b c)) ⇒ (↑(a ≤b c)))
BY
{ (ProvePropertyLemma `trans` 1 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[g:OCMon].  \mforall{}[a,b,c:|g|].    ((\muparrow{}(a  \mleq{}\msubb{}  b))  {}\mRightarrow{}  (\muparrow{}(b  \mleq{}\msubb{}  c))  {}\mRightarrow{}  (\muparrow{}(a  \mleq{}\msubb{}  c)))


By

---

Latex:
(ProvePropertyLemma  `trans`  1  THEN  Auto)\mcdot{}

---

Home Index