---

Step * of Lemma geo-line-eq_functionality

∀e:EuclideanPlane. ∀l,m,l1,m1:Line.  (l ≡ l1 ⇒ m ≡ m1 ⇒ (l ≡ m ⇐⇒ l1 ≡ m1))
BY
{ Auto }

1
1. e : EuclideanPlane
2. l : Line
3. m : Line
4. l1 : Line
5. m1 : Line
6. l ≡ l1
7. m ≡ m1
8. l ≡ m
⊢ l1 ≡ m1

2
1. e : EuclideanPlane
2. l : Line
3. m : Line
4. l1 : Line
5. m1 : Line
6. l ≡ l1
7. m ≡ m1
8. l1 ≡ m1
⊢ l ≡ m

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}l,m,l1,m1:Line.    (l  \mequiv{}  l1  {}\mRightarrow{}  m  \mequiv{}  m1  {}\mRightarrow{}  (l  \mequiv{}  m  \mLeftarrow{}{}\mRightarrow{}  l1  \mequiv{}  m1))


By

---

Latex:
Auto

---

Home Index