---

Step * 1 1 1 2 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. p ≠ m ∧ n
⊢ p ≠ m ∨ p ≠ l
BY
{ ((Assert n ≠ m BY EAuto 1) THEN RenameVar `t1' (-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. p ≠ m ∧ n
22. t1 : n ≠ m
⊢ 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
19.  m  \mwedge{}  n  \mneq{}  l
20.  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  n
21.  p  \mneq{}  m  \mwedge{}  n
\mvdash{}  p  \mneq{}  m  \mvee{}  p  \mneq{}  l


By

---

Latex:
((Assert  n  \mneq{}  m  BY  EAuto  1)  THEN  RenameVar  `t1'  (-1))

---

Home Index