---

Step * of Lemma geo-cong-preserves-bet-out

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.  (a_b_c ⇒ ab ≅ a'b' ⇒ ac ≅ a'c' ⇒ out(a' b'c') ⇒ a'_b'_c')
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN ((DoubleNegation THENM D 0) THENA Auto)
   THEN D -2
   THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a_b_c
9. ab ≅ a'b'
10. ac ≅ a'c'
11. a' ≠ b'
12. a' ≠ c'
13. ¬a'_b'_c'
14. a'_c'_b'
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  ((DoubleNegation  THENM  D  0)  THENA  Auto)
  THEN  D  -2
  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index