---

Step * of Lemma es-interval-one-one

∀[es:EO]. ∀[d,b,a,c:E].
  ({(a = c ∈ E) ∧ (b = d ∈ E)}) supposing (([a, b] = [c, d] ∈ (E List)) and c ≤loc d  and a ≤loc b )
BY
{ (Auto THEN Assert a = c ∈ E⋅) }

1
.....assertion..... 
1. es : EO
2. d : E
3. b : E
4. a : E
5. c : E
6. a ≤loc b 
7. c ≤loc d 
8. [a, b] = [c, d] ∈ (E List)
⊢ a = c ∈ E

2
1. es : EO
2. d : E
3. b : E
4. a : E
5. c : E
6. a ≤loc b 
7. c ≤loc d 
8. [a, b] = [c, d] ∈ (E List)
9. a = c ∈ E
⊢ {(a = c ∈ E) ∧ (b = d ∈ E)}

---

Latex:


\mforall{}[es:EO].  \mforall{}[d,b,a,c:E].
    (\{(a  =  c)  \mwedge{}  (b  =  d)\})  supposing  (([a,  b]  =  [c,  d])  and  c  \mleq{}loc  d    and  a  \mleq{}loc  b  )


By

(Auto  THEN  Assert  a  =  c\mcdot{})

---

Home Index