---

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

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
19. m ∧ n ≠ l
20. n ∧ l ≠ m ∧ n
21. n ∧ l ≠ p
⊢ p ≠ m ∨ p ≠ l

2
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. p ≠ m ∧ n
⊢ 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
18.  m  \mwedge{}  n  \mneq{}  m  \mwedge{}  l
\mvdash{}  p  \mneq{}  m  \mvee{}  p  \mneq{}  l


By

---

Latex:
((InstLemma  `pgeo-lsep-implies-plsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m  \mwedge{}  n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}s'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m  \mwedge{}  n\mkleeneclose{};\mkleeneopen{}n  \mwedge{}  l\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `pgeo-psep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n  \mwedge{}  l\mkleeneclose{};\mkleeneopen{}m  \mwedge{}  n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index