---

Step * of Lemma geo-extend-property

∀e:BasicGeometry. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c,d:Point.  (bextend ab by cd ≅ cd ∧ a_b_extend ab by cd)
BY
{ ((UnivCD THENA Auto) THEN (GenConclTerm ⌜extend ab by cd⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : Point
5. d : Point
6. v : {x:Point| a_b_x ∧ bx ≅ cd} 
7. extend ab by cd = v ∈ {x:Point| a_b_x ∧ bx ≅ cd} 
⊢ bv ≅ cd ∧ a_b_v

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .  \mforall{}c,d:Point.
    (bextend  ab  by  cd  \00D0  cd  \mwedge{}  a\_b\_extend  ab  by  cd)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}extend  ab  by  cd\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index