---

Step * 1 1 of Lemma geo-strict-between_functionality


1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. a1 ≡ a2
9. b1 ≡ b2
10. c1 ≡ c2
11. a1_b1_c1 ∧ a1 ≠ b1 ∧ b1 ≠ c1
⊢ a2_b2_c2 ∧ a2 ≠ b2 ∧ b2 ≠ c2
BY
{ (RWO "-4 -3 -2" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  a1  \mequiv{}  a2
9.  b1  \mequiv{}  b2
10.  c1  \mequiv{}  c2
11.  a1\_b1\_c1  \mwedge{}  a1  \mneq{}  b1  \mwedge{}  b1  \mneq{}  c1
\mvdash{}  a2\_b2\_c2  \mwedge{}  a2  \mneq{}  b2  \mwedge{}  b2  \mneq{}  c2


By

---

Latex:
(RWO  "-4  -3  -2"  (-1)  THEN  Auto)

---

Home Index