Step
*
1
1
1
1
2
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. s : a1 ≠ b1
25. b1 ≠ c1
26. c1 ≠ a1
27. s1 : b1 ≠ a
28. a1 ≠ b1 ∨ a
⊢ ∃p:Point. p ≠ l
BY
{ ((InstLemma `LP-sep-or2` [⌜g⌝;⌜b1 ∨ a⌝;⌜a1⌝;⌜q⌝]⋅ THEN Auto) THEN D -1) }
1
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
29. q ≠ b1 ∨ a
⊢ ∃p:Point. p ≠ l
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
29. q ≠ a1
⊢ ∃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. s : a1 \mneq{} b1
25. b1 \mneq{} c1
26. c1 \mneq{} a1
27. s1 : b1 \mneq{} a
28. a1 \mneq{} b1 \mvee{} a
\mvdash{} \mexists{}p:Point. p \mneq{} l
By
Latex:
((InstLemma `LP-sep-or2` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b1 \mvee{} a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{} THEN Auto) THEN D -1)
Home
Index