---

Step * 1 2 1 of Lemma geo-vert-angle-SAS

.....assertion..... 
1. e : BasicGeometry
2. a : Point
3. p : Point
4. q : Point
5. p' : Point
6. q' : Point
7. p-a-q'
8. p'-a-q'
9. pa ≅ p'a
10. q'a ≅ q'a
11. p ≠ p'
12. q ≡ q'
⊢ False
BY
{ ((((InstLemma `geo-out-iff-between1` [⌜e⌝;⌜a⌝;⌜p⌝;⌜p'⌝;⌜q'⌝]⋅ THENA Auto)
     THEN FLemma `geo-strict-between-implies-between` [-6]
     )
    THEN Auto
    )
   THEN FLemma `geo-out-unicity` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  q  :  Point
5.  p'  :  Point
6.  q'  :  Point
7.  p-a-q'
8.  p'-a-q'
9.  pa  \mcong{}  p'a
10.  q'a  \mcong{}  q'a
11.  p  \mneq{}  p'
12.  q  \mequiv{}  q'
\mvdash{}  False


By

---

Latex:
((((InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}q'\mkleeneclose{}]\mcdot{}  THENA  Auto)
      THEN  FLemma  `geo-strict-between-implies-between`  [-6]
      )
    THEN  Auto
    )
  THEN  FLemma  `geo-out-unicity`  [-1]
  THEN  Auto)

---

Home Index