---

Step * of Lemma ocmon_trans

∀[g:OCMon]. ∀[a,b,c:|g|].  (↑(a ≤b c)) supposing ((↑(b ≤b c)) and (↑(a ≤b b)))
BY
{ Assert ⌜∀[g:OCMon]. ∀[a,b,c:|g|].  ((↑(a ≤b b)) ⇒ (↑(b ≤b c)) ⇒ (↑(a ≤b c)))⌝⋅ }

1
.....assertion..... 
∀[g:OCMon]. ∀[a,b,c:|g|].  ((↑(a ≤b b)) ⇒ (↑(b ≤b c)) ⇒ (↑(a ≤b c)))

2
1. ∀[g:OCMon]. ∀[a,b,c:|g|].  ((↑(a ≤b b)) ⇒ (↑(b ≤b c)) ⇒ (↑(a ≤b c)))
⊢ ∀[g:OCMon]. ∀[a,b,c:|g|].  (↑(a ≤b c)) supposing ((↑(b ≤b c)) and (↑(a ≤b b)))

---

Latex:

---

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


By

---

Latex:
Assert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}

---

Home Index