---

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


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
BY
{ ∀h:hyp. (FLemma  `geo-add-length-between` [h] THENA 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'
15. |a'b'| = |a'c'| + |c'b'| ∈ Length
16. |ac| = |ab| + |bc| ∈ Length
⊢ False

---

Latex:

---

Latex:

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  \00D0  a'b'
10.  ac  \00D0  a'c'
11.  a'  \mneq{}  b'
12.  a'  \mneq{}  c'
13.  \mneg{}a'\_b'\_c'
14.  a'\_c'\_b'
\mvdash{}  False


By

---

Latex:
\mforall{}h:hyp.  (FLemma    `geo-add-length-between`  [h]  THENA  Auto) 

---

Home Index