---

Step * of Lemma p2J_symmetry

∀[a,b:ℙ^2].  p2J(a;b) = p2J(b;a) supposing a ≠ b
BY
{ (Auto THEN FLemma  `proj-sep_symmetry` [3] THEN Auto THEN (BLemma `proj-eq-iff` THEN Auto) THEN D 0 THEN Reduce 0) }

1
1. a : ℙ^2
2. b : ℙ^2
3. a ≠ b
4. b ≠ a
⊢ ∃m:{m:ℝ| m ≠ r0} . req-vec(3;p2J(a;b);m*p2J(b;a))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  FLemma    `proj-sep\_symmetry`  [3]
  THEN  Auto
  THEN  (BLemma  `proj-eq-iff`  THEN  Auto)
  THEN  D  0
  THEN  Reduce  0)

---

Home Index