---

Step * of Lemma projective-plane-axioms

∀g:ProjectivePlane
  ((∀p,q,r:Point. ∀s:p ≠ q. ∀s1:q ≠ r.  (r ≠ p ∨ q ⇒ p ≠ q ∨ r))
  ∧ (∀p,q:Point. ∀l,m:Line. ∀s:p ≠ q. ∀s1:l ≠ m.  (p ≠ l ⇒ q ≠ m ⇒ p I m ⇒ q I l ⇒ l ∧ m ≠ p ∨ q)))
BY
{ (((Auto THEN D 1 THEN Unhide) THENA Auto) THEN ExRepD) }

1
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

2
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

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane
    ((\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))
    \mwedge{}  (\mforall{}p,q:Point.  \mforall{}l,m:Line.  \mforall{}s:p  \mneq{}  q.  \mforall{}s1:l  \mneq{}  m.
              (p  \mneq{}  l  {}\mRightarrow{}  q  \mneq{}  m  {}\mRightarrow{}  p  I  m  {}\mRightarrow{}  q  I  l  {}\mRightarrow{}  l  \mwedge{}  m  \mneq{}  p  \mvee{}  q)))


By

---

Latex:
(((Auto  THEN  D  1  THEN  Unhide)  THENA  Auto)  THEN  ExRepD)

---

Home Index