Step * 1 1 of Lemma symmetric-point-construction1

.....antecedent..... 
1. BasicGeometry
2. Point
3. Point
4. [%1] 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