---

Step * of Lemma point-implies-plsep-exists

∀g:ProjectivePlane. ∀a:Point.  ∃l:Line. a ≠ l
BY
{ (((((Auto THEN InstLemma `pgeo-three-lines-axiom` [⌜g⌝;⌜a⌝]⋅ THEN Auto) THEN ExRepD)
     THEN ((Duplicate 9 THEN D -1) THEN InstLemma `pgeo-three-points-axiom` [⌜g⌝;⌜m⌝]⋅ THEN Auto)
     THEN ExRepD)
    THEN (Duplicate 21 THEN D -1)
    THEN ExRepD)
   THEN (InstLemma `LP-sep-or` [⌜g⌝;⌜l1⌝;⌜b⌝;⌜a⌝]⋅ THEN Auto)
   THEN D -1) }

1
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. a ≠ l1
⊢ ∃l:Line. a ≠ l

2
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. a ≠ b
⊢ ∃l:Line. a ≠ l

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}a:Point.    \mexists{}l:Line.  a  \mneq{}  l


By

---

Latex:
(((((Auto  THEN  InstLemma  `pgeo-three-lines-axiom`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
      THEN  ((Duplicate  9  THEN  D  -1)  THEN  InstLemma  `pgeo-three-points-axiom`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)
      THEN  ExRepD)
    THEN  (Duplicate  21  THEN  D  -1)
    THEN  ExRepD)
  THEN  (InstLemma  `LP-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1)

---

Home Index