---

Step * of Lemma geo-bet-sep-cong-tri-exists

∀e:BasicGeometry. ∀a,b,c,a',c':Point.
  (a ≠ b ⇒ (∃b':Point. (a'_b'_c' ∧ Cong3(abc,a'b'c'))) supposing (a_b_c and ac ≅ a'c'))
BY
{ (InstLemma `geo-congruent-between-exists` [] THEN RepeatFor 11 ((ParallelLast' THENA Auto)) THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',c':Point.
    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}b':Point.  (a'\_b'\_c'  \mwedge{}  Cong3(abc,a'b'c')))  supposing  (a\_b\_c  and  ac  \00D0  a'c'))


By

---

Latex:
(InstLemma  `geo-congruent-between-exists`  []
  THEN  RepeatFor  11  ((ParallelLast'  THENA  Auto))
  THEN  D  0
  THEN  Auto)

---

Home Index