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