---

Step * of Lemma geo-plsep_functionality

No Annotations
∀e:EuclideanPlane. ∀a1,a2:Point. ∀l1,l2:Line.  (a1 ≡ a2 ⇒ l1 ≡ l2 ⇒ (a1 # l1 ⇐⇒ a2 # l2))
BY
{ (Auto
   THEN (Unfold `geo-plsep` -1 THEN Unfold `geo-plsep` 0)
   THEN (InstLemma `geo-line-eq-to-col` [⌜e⌝;⌜l1⌝;⌜l2⌝]⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. l1 : Line
5. l2 : Line
6. a1 ≡ a2
7. l1 ≡ l2
8. a1 # fst(l1)fst(snd(l1))
9. Colinear(fst(l1);fst(snd(l1));fst(l2)) ∧ Colinear(fst(l1);fst(snd(l1));fst(snd(l2)))
⊢ a2 # fst(l2)fst(snd(l2))

2
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. l1 : Line
5. l2 : Line
6. a1 ≡ a2
7. l1 ≡ l2
8. a2 # fst(l2)fst(snd(l2))
9. Colinear(fst(l1);fst(snd(l1));fst(l2)) ∧ Colinear(fst(l1);fst(snd(l1));fst(snd(l2)))
⊢ a1 # fst(l1)fst(snd(l1))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a1,a2:Point.  \mforall{}l1,l2:Line.    (a1  \mequiv{}  a2  {}\mRightarrow{}  l1  \mequiv{}  l2  {}\mRightarrow{}  (a1  \#  l1  \mLeftarrow{}{}\mRightarrow{}  a2  \#  l2))


By

---

Latex:
(Auto
  THEN  (Unfold  `geo-plsep`  -1  THEN  Unfold  `geo-plsep`  0)
  THEN  (InstLemma  `geo-line-eq-to-col`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}l2\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index