---

Step * of Lemma geo-out-unicity

∀e:BasicGeometry. ∀a,b,c:Point.  (out(a bc) ⇒ ab ≅ ac ⇒ b ≡ c)
BY
{ (Auto
   THEN RepeatFor 2 (D -2)
   THEN Unfold `geo-eq` 0
   THEN ParallelOp -2
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN MoveToConcl (-2)
   THEN Fold `not` 0
   THEN Fold `geo-eq` 0
   THEN (FLemma  `geo-add-length-between` [-1] THENA Auto)
   THEN (Assert |ac| = |ab| ∈ Length BY
               Auto)
   THEN (RWO  "-1" (-2) THENA Auto)
   THEN FLemma `geo-add-length-implies-eq` [-2]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (out(a  bc)  {}\mRightarrow{}  ab  \00D0  ac  {}\mRightarrow{}  b  \mequiv{}  c)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -2)
  THEN  Unfold  `geo-eq`  0
  THEN  ParallelOp  -2
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  Fold  `not`  0
  THEN  Fold  `geo-eq`  0
  THEN  (FLemma    `geo-add-length-between`  [-1]  THENA  Auto)
  THEN  (Assert  |ac|  =  |ab|  BY
                          Auto)
  THEN  (RWO    "-1"  (-2)  THENA  Auto)
  THEN  FLemma  `geo-add-length-implies-eq`  [-2]
  THEN  Auto)

---

Home Index