---

Step * 2 1 of Lemma point-implies-plsep-exists

.....antecedent..... 
1. g : ProjectivePlane
2. a : Point
3. l : Line
4. m : Line
5. n : Line
6. a I l
7. a I m
8. a I n
9. l ≠ m
10. m ≠ n
11. n ≠ l
12. a1 : Point
13. a1 I l
14. a1 ≠ m
15. a2 : Point
16. b : Point
17. c : Point
18. a2 I m
19. b I m
20. c I m
21. a2 ≠ b
22. b ≠ c
23. c ≠ a2
24. l1 : Line
25. a2 I l1
26. b ≠ l1
27. s : a ≠ b
28. s1 : b ≠ a1
⊢ a1 ≠ a ∨ b
BY
{ (InstLemma `pgeo-plsep-implies-join` [⌜g⌝;⌜a1⌝;⌜m⌝;⌜a⌝;⌜b⌝;⌜s⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  ProjectivePlane
2.  a  :  Point
3.  l  :  Line
4.  m  :  Line
5.  n  :  Line
6.  a  I  l
7.  a  I  m
8.  a  I  n
9.  l  \mneq{}  m
10.  m  \mneq{}  n
11.  n  \mneq{}  l
12.  a1  :  Point
13.  a1  I  l
14.  a1  \mneq{}  m
15.  a2  :  Point
16.  b  :  Point
17.  c  :  Point
18.  a2  I  m
19.  b  I  m
20.  c  I  m
21.  a2  \mneq{}  b
22.  b  \mneq{}  c
23.  c  \mneq{}  a2
24.  l1  :  Line
25.  a2  I  l1
26.  b  \mneq{}  l1
27.  s  :  a  \mneq{}  b
28.  s1  :  b  \mneq{}  a1
\mvdash{}  a1  \mneq{}  a  \mvee{}  b


By

---

Latex:
(InstLemma  `pgeo-plsep-implies-join`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index