---

Step * 2 of Lemma projective-plane-axioms


1. g : ProjectivePlaneStructure
2. BasicProjectiveGeometryAxioms(g)
3. triangle-axiom1(g)
4. triangle-axiom2(g)
5. ∀p,q,r:Point. ∀s:p ≠ q. ∀s1:q ≠ r.  (r ≠ p ∨ q ⇒ p ≠ q ∨ r)
6. p : Point
7. q : Point
8. l : Line
9. m : Line
10. s : p ≠ q
11. s1 : l ≠ m
12. p ≠ l
13. q ≠ m
14. p I m
15. q I l
⊢ l ∧ m ≠ p ∨ q
BY
{ (Unfold `triangle-axiom2` 4 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlaneStructure
2.  BasicProjectiveGeometryAxioms(g)
3.  triangle-axiom1(g)
4.  triangle-axiom2(g)
5.  \mforall{}p,q,r:Point.  \mforall{}s:p  \mneq{}  q.  \mforall{}s1:q  \mneq{}  r.    (r  \mneq{}  p  \mvee{}  q  {}\mRightarrow{}  p  \mneq{}  q  \mvee{}  r)
6.  p  :  Point
7.  q  :  Point
8.  l  :  Line
9.  m  :  Line
10.  s  :  p  \mneq{}  q
11.  s1  :  l  \mneq{}  m
12.  p  \mneq{}  l
13.  q  \mneq{}  m
14.  p  I  m
15.  q  I  l
\mvdash{}  l  \mwedge{}  m  \mneq{}  p  \mvee{}  q


By

---

Latex:
(Unfold  `triangle-axiom2`  4  THEN  Auto)

---

Home Index