---

Step * 1 1 1 1 of Lemma line-implies-plsep-exists


1. g : ProjectivePlane
2. l : Line
3. a : Point
4. b : Point
5. c : Point
6. a I l
7. b I l
8. c I l
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. m : Line
13. a ≠ m
14. l ≠ m
15. q : Point
16. q I l
17. q I m
18. a1 : Point
19. b1 : Point
20. c1 : Point
21. a1 I m
22. b1 I m
23. c1 I m
24. a1 ≠ b1
25. b1 ≠ c1
26. c1 ≠ a1
⊢ ∃p:Point. p ≠ l
BY
{ ((Assert b1 ≠ a BY
          (InstLemma `pgeo-plsep-to-psep` [⌜g⌝;⌜a⌝;⌜b1⌝;⌜m⌝] ⋅ THEN Auto))
   THEN (RenameVar `s' (24) THEN RenameVar `s1' (27))
   THEN (InstLemma `use-triangle-axiom1` [⌜g⌝;⌜a1⌝;⌜b1⌝;⌜a⌝;⌜s⌝;⌜s1⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
1. g : ProjectivePlane
2. l : Line
3. a : Point
4. b : Point
5. c : Point
6. a I l
7. b I l
8. c I l
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. m : Line
13. a ≠ m
14. l ≠ m
15. q : Point
16. q I l
17. q I m
18. a1 : Point
19. b1 : Point
20. c1 : Point
21. a1 I m
22. b1 I m
23. c1 I m
24. s : a1 ≠ b1
25. b1 ≠ c1
26. c1 ≠ a1
27. s1 : b1 ≠ a
⊢ a ≠ a1 ∨ b1

2
1. g : ProjectivePlane
2. l : Line
3. a : Point
4. b : Point
5. c : Point
6. a I l
7. b I l
8. c I l
9. a ≠ b
10. b ≠ c
11. c ≠ a
12. m : Line
13. a ≠ m
14. l ≠ m
15. q : Point
16. q I l
17. q I m
18. a1 : Point
19. b1 : Point
20. c1 : Point
21. a1 I m
22. b1 I m
23. c1 I m
24. s : a1 ≠ b1
25. b1 ≠ c1
26. c1 ≠ a1
27. s1 : b1 ≠ a
28. a1 ≠ b1 ∨ a
⊢ ∃p:Point. p ≠ l

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  l  :  Line
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  a  I  l
7.  b  I  l
8.  c  I  l
9.  a  \mneq{}  b
10.  b  \mneq{}  c
11.  c  \mneq{}  a
12.  m  :  Line
13.  a  \mneq{}  m
14.  l  \mneq{}  m
15.  q  :  Point
16.  q  I  l
17.  q  I  m
18.  a1  :  Point
19.  b1  :  Point
20.  c1  :  Point
21.  a1  I  m
22.  b1  I  m
23.  c1  I  m
24.  a1  \mneq{}  b1
25.  b1  \mneq{}  c1
26.  c1  \mneq{}  a1
\mvdash{}  \mexists{}p:Point.  p  \mneq{}  l


By

---

Latex:
((Assert  b1  \mneq{}  a  BY
                (InstLemma  `pgeo-plsep-to-psep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  \mcdot{}  THEN  Auto))
  THEN  (RenameVar  `s'  (24)  THEN  RenameVar  `s1'  (27))
  THEN  (InstLemma  `use-triangle-axiom1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}s1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index