---

Step * of Lemma pgeo-plsep_functionality

∀g:ProjectivePlane. ∀a,a1:Point. ∀l,l1:Line.  (a ≡ a1 ⇒ l ≡ l1 ⇒ {a ≠ l ⇐⇒ a1 ≠ l1})
BY
{ (Unfold `guard` 0 THEN Auto) }

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

2
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

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}a,a1:Point.  \mforall{}l,l1:Line.    (a  \mequiv{}  a1  {}\mRightarrow{}  l  \mequiv{}  l1  {}\mRightarrow{}  \{a  \mneq{}  l  \mLeftarrow{}{}\mRightarrow{}  a1  \mneq{}  l1\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index