---

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


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
14. xx : l ≠ n
15. t1' : m ≠ n
16. s' : m ≠ l
17. t : n ≠ l
18. m ∧ n ≠ m ∧ l
19. m ∧ n ≠ l
20. n ∧ l ≠ m ∧ n
21. n ∧ l ≠ p
⊢ p ≠ m ∨ p ≠ l
BY
{ (((FLemma `pgeo-psep-sym` [-1]⋅ THENA Auto)
    THEN (InstLemma `pgeo-lsep-implies-plsep` [⌜g⌝;⌜p⌝;⌜n⌝;⌜l⌝;⌜t⌝]⋅ THENA Auto)
    )
   THEN OrRight⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  p  :  Point
3.  l  :  Line
4.  m  :  Line
5.  s  :  l  \mneq{}  m
6.  s1  :  p  \mneq{}  l  \mwedge{}  m
7.  a  :  Point
8.  a  I  m
9.  a  \mneq{}  l
10.  p  \mneq{}  a
11.  n  :  Line
12.  p  I  n
13.  l  \mwedge{}  m  \mneq{}  n
14.  xx  :  l  \mneq{}  n
15.  t1'  :  m  \mneq{}  n
16.  s'  :  m  \mneq{}  l
17.  t  :  n  \mneq{}  l
18.  m  \mwedge{}  n  \mneq{}  m  \mwedge{}  l
19.  m  \mwedge{}  n  \mneq{}  l
20.  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  n
21.  n  \mwedge{}  l  \mneq{}  p
\mvdash{}  p  \mneq{}  m  \mvee{}  p  \mneq{}  l


By

---

Latex:
(((FLemma  `pgeo-psep-sym`  [-1]\mcdot{}  THENA  Auto)
    THEN  (InstLemma  `pgeo-lsep-implies-plsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  OrRight\mcdot{}
  THEN  Auto)

---

Home Index