---

Step * 1 of Lemma geo-add-length-zero


1. e : BasicGeometry
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
5. x ∈ {p:Point| O_X_p} 
6. x1 ∈ {p:Point| O_X_p} 
7. x ≡ x1
⊢ extend Ox by XX ≡ x1
BY
{ (InstLemma `geo-eq_transitivity` [⌜e⌝;⌜extend Ox by XX⌝;⌜x⌝;⌜x1⌝]⋅
   THEN Auto
   THEN ThinVar `x1'
   THEN RenameTo `a' `x'
   THEN (GenConcl ⌜a = x ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. e : BasicGeometry
2. x : {p:Point| O_X_p} 
⊢ extend Ox by XX ≡ x

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Base
3.  x1  :  Base
4.  x  =  x1
5.  x  \mmember{}  \{p:Point|  O\_X\_p\} 
6.  x1  \mmember{}  \{p:Point|  O\_X\_p\} 
7.  x  \mequiv{}  x1
\mvdash{}  extend  Ox  by  XX  \mequiv{}  x1


By

---

Latex:
(InstLemma  `geo-eq\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}extend  Ox  by  XX\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ThinVar  `x1'
  THEN  RenameTo  `a'  `x'
  THEN  (GenConcl  \mkleeneopen{}a  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index