---

Step * 1 of Lemma pgeo-meet-implies-psep2


1. g : ProjectivePlane
2. l : Line
3. m : Line
4. s : l ≠ m
5. a : Point
6. c : {c:Point| c I l ∧ c I m} 
7. l1 : Line
8. a I l1
9. c ≠ l1
10. a I l1
11. l ∧ m ≠ c
⊢ l ∧ m ≠ l1
BY
{ ((InstLemma `pgeo-meet-to-point` [⌜g⌝;⌜l⌝;⌜m⌝;⌜c⌝;⌜s⌝]⋅ THENA Auto)
   THEN D -1
   THEN FLemma `pgeo-psep-sym` [-1]
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  l  :  Line
3.  m  :  Line
4.  s  :  l  \mneq{}  m
5.  a  :  Point
6.  c  :  \{c:Point|  c  I  l  \mwedge{}  c  I  m\} 
7.  l1  :  Line
8.  a  I  l1
9.  c  \mneq{}  l1
10.  a  I  l1
11.  l  \mwedge{}  m  \mneq{}  c
\mvdash{}  l  \mwedge{}  m  \mneq{}  l1


By

---

Latex:
((InstLemma  `pgeo-meet-to-point`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  FLemma  `pgeo-psep-sym`  [-1]
  THEN  Auto)

---

Home Index