---

Step * 2 of Lemma pgeo-plsep_functionality


1. g : ProjectivePlane
2. a : Point
3. a1 : Point
4. l : Line
5. l1 : Line
6. a ≡ a1
7. l ≡ l1
8. a1 ≠ l1
⊢ a ≠ l
BY
{ (SwapVars `a' `a1' THEN SwapVars `l' `l1') }

1
1. g : ProjectivePlane
2. a1 : Point
3. a : Point
4. l1 : Line
5. l : Line
6. a1 ≡ a
7. l1 ≡ l
8. a ≠ l
⊢ a1 ≠ l1

---

Latex:

---

Latex:

1.  g  :  ProjectivePlane
2.  a  :  Point
3.  a1  :  Point
4.  l  :  Line
5.  l1  :  Line
6.  a  \mequiv{}  a1
7.  l  \mequiv{}  l1
8.  a1  \mneq{}  l1
\mvdash{}  a  \mneq{}  l


By

---

Latex:
(SwapVars  `a'  `a1'  THEN  SwapVars  `l'  `l1')

---

Home Index