---

Step * 1 of Lemma projective-plane-axioms


1. g : ProjectivePlaneStructure
2. BasicProjectiveGeometryAxioms(g)
3. triangle-axiom1(g)
4. triangle-axiom2(g)
5. p : Point
6. q : Point
7. r : Point
8. s : p ≠ q
9. s1 : q ≠ r
10. r ≠ p ∨ q
⊢ p ≠ q ∨ r
BY
{ (Unfold `triangle-axiom1` 3 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlaneStructure
2.  BasicProjectiveGeometryAxioms(g)
3.  triangle-axiom1(g)
4.  triangle-axiom2(g)
5.  p  :  Point
6.  q  :  Point
7.  r  :  Point
8.  s  :  p  \mneq{}  q
9.  s1  :  q  \mneq{}  r
10.  r  \mneq{}  p  \mvee{}  q
\mvdash{}  p  \mneq{}  q  \mvee{}  r


By

---

Latex:
(Unfold  `triangle-axiom1`  3  THEN  Auto)

---

Home Index