---

Step * of Lemma geo-extend-property1

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

1
1. e : BasicGeometry
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : Point
5. d : Point
6. v : Point
7. a_b_v
8. bv ≅ cd
9. extend ab by cd = v ∈ {x:Point| a_b_x ∧ bx ≅ cd} 
10. bv ≅ cd
11. c ≠ d
⊢ 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{}  (c  \mneq{}  d  {}\mRightarrow{}  a-b-extend  ab  by  cd))


By

---

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

---

Home Index