---

Step * 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
⊢ p ≠ m ∨ p ≠ l
BY
{ (InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜m ∧ l⌝;⌜m ∧ n⌝;⌜n⌝]⋅
   THENA (Auto THEN InstLemma `pgeo-meet-plsep-sym` [⌜g⌝;⌜l⌝;⌜m⌝;⌜n⌝;⌜s⌝;⌜s'⌝]⋅ THEN Auto)
   ) }

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
14. xx : l ≠ n
15. t1' : m ≠ n
16. s' : m ≠ l
17. t : n ≠ l
18. m ∧ n ≠ m ∧ l
⊢ p ≠ m ∨ p ≠ l

---

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
\mvdash{}  p  \mneq{}  m  \mvee{}  p  \mneq{}  l


By

---

Latex:
(InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m  \mwedge{}  l\mkleeneclose{};\mkleeneopen{}m  \mwedge{}  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  InstLemma  `pgeo-meet-plsep-sym`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}s'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  )

---

Home Index