---

Step * of Lemma proj-sep_symmetry

∀n:ℕ. ∀a,b:ℙ^n.  (a ≠ b ⇒ b ≠ a)
BY
{ (Auto THEN RepeatFor 2 (ParallelLast)) }

1
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. u(a) ≠ r(-1)*u(b)
5. u(a) ≠ u(b)
⊢ u(b) ≠ u(a)

2
1. n : ℕ
2. a : ℙ^n
3. b : ℙ^n
4. u(a) ≠ u(b)
5. u(a) ≠ r(-1)*u(b)
⊢ u(b) ≠ r(-1)*u(a)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbP{}\^{}n.    (a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  a)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast))

---

Home Index