---

Step * of Lemma pgeo-lsep-implies-plsep-or

∀g:ProjectivePlane. ∀p:Point. ∀l,m:Line. ∀s:l ≠ m.  (p ≠ l ∧ m ⇒ (p ≠ m ∨ p ≠ l))
BY
{ ((Auto THEN (((Assert m ≠ l BY EAuto 1) THEN D -1) THEN ExRepD) THEN RenameVar`s1' (6))
   THEN (((InstLemma `LP-sep-or2` [⌜g⌝;⌜l⌝;⌜a⌝;⌜p⌝]⋅ THEN Auto) THEN D -1) THEN Auto)
   THEN (((Assert p ≠ l ∧ m BY Auto) THEN Unfold `pgeo-psep` -1 THEN Auto) THEN ExRepD)
   THEN RenameVar `n'(-3)) }

1
1. g : ProjectivePlane
2. p : Point
3. l : Line
4. m : Line
5. s : l ≠ m
6. s1 : p ≠ l ∧ m
7. a : Point
8. a I m
9. a ≠ l
10. p ≠ a
11. n : Line
12. p I n
13. l ∧ m ≠ n
⊢ p ≠ m ∨ p ≠ l

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}p:Point.  \mforall{}l,m:Line.  \mforall{}s:l  \mneq{}  m.    (p  \mneq{}  l  \mwedge{}  m  {}\mRightarrow{}  (p  \mneq{}  m  \mvee{}  p  \mneq{}  l))


By

---

Latex:
((Auto  THEN  (((Assert  m  \mneq{}  l  BY  EAuto  1)  THEN  D  -1)  THEN  ExRepD)  THEN  RenameVar`s1'  (6))
  THEN  (((InstLemma  `LP-sep-or2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1)  THEN  Auto)
  THEN  (((Assert  p  \mneq{}  l  \mwedge{}  m  BY  Auto)  THEN  Unfold  `pgeo-psep`  -1  THEN  Auto)  THEN  ExRepD)
  THEN  RenameVar  `n'(-3))

---

Home Index