---

Step * 2 of Lemma lsep-symmetry


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
⊢ c # ab
BY
{ (Unfold `geo-lsep` 0 THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  c  \#  ba
\mvdash{}  c  \#  ab


By

---

Latex:
(Unfold  `geo-lsep`  0  THEN  D  -1  THEN  Auto)

---

Home Index