---

Step * 1 of Lemma es-causle-trans


1. the_es : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. (a < b) ∨ (a = b ∈ E)@i
6. (b < c) ∨ (b = c ∈ E)@i
7. Trans(E;e,e'.(e < e'))
⊢ (a < c) ∨ (a = c ∈ E)
BY
{ ((SplitOrHyps
    THENL [(OrLeft THENM UseTrans ⌜b⌝⋅); (OrLeft THENM (HypSubst (-3) 0)); (OrLeft THENM (HypSubst (-2) (-3))); OrRight]
   )
   THEN Auto
   )⋅ }

---

Latex:

---

Latex:

1.  the$_{es}$  :  EO@i'
2.  a  :  E@i
3.  b  :  E@i
4.  c  :  E@i
5.  (a  <  b)  \mvee{}  (a  =  b)@i
6.  (b  <  c)  \mvee{}  (b  =  c)@i
7.  Trans(E;e,e'.(e  <  e'))
\mvdash{}  (a  <  c)  \mvee{}  (a  =  c)


By

---

Latex:
((SplitOrHyps
    THENL  [(OrLeft  THENM  UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{})
                ;  (OrLeft  THENM  (HypSubst  (-3)  0))
                ;  (OrLeft  THENM  (HypSubst  (-2)  (-3)))
                ;  OrRight]
  )
  THEN  Auto
  )\mcdot{}

---

Home Index