---

Step * 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. ∃l:Line. a ≠ l
⊢ ∃p:Point. p ≠ l
BY
{ ((ExRepD THEN RenameVar `m' (12))
   THEN (Assert l ≠ m BY
               (InstLemma `pgeo-plsep-to-lsep` [⌜g⌝;⌜m⌝;⌜l⌝;⌜a⌝]⋅ THEN Auto))
   ) }

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
⊢ ∃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.  \mexists{}l:Line.  a  \mneq{}  l
\mvdash{}  \mexists{}p:Point.  p  \mneq{}  l


By

---

Latex:
((ExRepD  THEN  RenameVar  `m'  (12))
  THEN  (Assert  l  \mneq{}  m  BY
                          (InstLemma  `pgeo-plsep-to-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto))
  )

---

Home Index