---

Step * 1 of Lemma proj-sep_functionality

.....assertion..... 
∀n:ℕ. ∀a1,b1,a2,b2:ℙ^n.  (a1 = a2 ⇒ b1 = b2 ⇒ a1 ≠ b1 ⇒ a2 ≠ b2)
BY
{ (Auto THEN (All  (RWO "not-proj-sep-iff-proj-eq<") THENA Auto)) }

1
1. n : ℕ
2. a1 : ℙ^n
3. b1 : ℙ^n
4. a2 : ℙ^n
5. b2 : ℙ^n
6. ¬a1 ≠ a2
7. ¬b1 ≠ b2
8. a1 ≠ b1
⊢ a2 ≠ b2

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n:\mBbbN{}.  \mforall{}a1,b1,a2,b2:\mBbbP{}\^{}n.    (a1  =  a2  {}\mRightarrow{}  b1  =  b2  {}\mRightarrow{}  a1  \mneq{}  b1  {}\mRightarrow{}  a2  \mneq{}  b2)


By

---

Latex:
(Auto  THEN  (All    (RWO  "not-proj-sep-iff-proj-eq<")  THENA  Auto))

---

Home Index