---

Step * of Lemma LP-sep-or2

∀g:ProjectivePlaneStructure. ∀l:Line. ∀p,q:Point.  (p ≠ l ⇒ (q ≠ l ∨ q ≠ p))
BY
{ (Auto THEN Assert ⌜l ≠ p⌝⋅) }

1
.....assertion..... 
1. g : ProjectivePlaneStructure
2. l : Line
3. p : Point
4. q : Point
5. p ≠ l
⊢ l ≠ p

2
1. g : ProjectivePlaneStructure
2. l : Line
3. p : Point
4. q : Point
5. p ≠ l
6. l ≠ p
⊢ q ≠ l ∨ q ≠ p

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure.  \mforall{}l:Line.  \mforall{}p,q:Point.    (p  \mneq{}  l  {}\mRightarrow{}  (q  \mneq{}  l  \mvee{}  q  \mneq{}  p))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}l  \mneq{}  p\mkleeneclose{}\mcdot{})

---

Home Index