---

Step * 1 3 2 of Lemma pgeo-triangle-dual


1. pg : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : b ≠ c
6. t4 : a ≠ b ∨ c
7. s2 : a ≠ b
8. s3 : c ≠ a
9. s4 : b ∨ c ≠ c ∨ a
10. s5 : a ∨ b ≠ b ∨ c ∨ c ∨ a
⊢ let a@0,b@0,c@0,s@0,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = <a ∨ b, b ∨ c, c ∨ a, s4, s5> in a@0 I lab ∧ b@0 \000CI lab ∧ b@0 I lbc ∧ c@0 I lbc ∧ c@0 I lca ∧ a@0 I lca
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  s  :  b  \mneq{}  c
6.  t4  :  a  \mneq{}  b  \mvee{}  c
7.  s2  :  a  \mneq{}  b
8.  s3  :  c  \mneq{}  a
9.  s4  :  b  \mvee{}  c  \mneq{}  c  \mvee{}  a
10.  s5  :  a  \mvee{}  b  \mneq{}  b  \mvee{}  c  \mvee{}  c  \mvee{}  a
\mvdash{}  let  a@0,b@0,c@0,s@0,s'  =  <a,  b,  c,  s,  t4>  in  let  lab,lbc,lca,s1,s2  =  <a  \mvee{}  b,  b  \mvee{}  c,  c  \mvee{}  a,  s4,  s5>\000C  in  a@0  I  lab
\mwedge{}  b@0  I  lab
\mwedge{}  b@0  I  lbc
\mwedge{}  c@0  I  lbc
\mwedge{}  c@0  I  lca
\mwedge{}  a@0  I  lca


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index