---

Step * 1 1 of Lemma symmetric-point-construction1

.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. p : Point
4. [%1] : a # p
⊢ p # a
BY
{ (BLemma `geo-sep-sym` THEN Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  [\%1]  :  a  \#  p
\mvdash{}  p  \#  a


By

---

Latex:
(BLemma  `geo-sep-sym`  THEN  Auto  THEN  Unhide  THEN  Auto)

---

Home Index