---

Step * of Lemma p2J_on_symm

∀[a,b:ℙ^2].  p2J(a;b) on b supposing a ≠ b
BY
{ (Auto THEN (FLemma `proj-sep_symmetry` [-1] THENA Auto) THEN RWO "p2J_symmetry" 0 THEN Auto) }

1
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. b ≠ a
⊢ p2J(b;a) on b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbP{}\^{}2].    p2J(a;b)  on  b  supposing  a  \mneq{}  b


By

---

Latex:
(Auto  THEN  (FLemma  `proj-sep\_symmetry`  [-1]  THENA  Auto)  THEN  RWO  "p2J\_symmetry"  0  THEN  Auto)

---

Home Index