---

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

.....wf..... 
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
11. t* : pgeo-triangle(pg*)
⊢ let a,b,c,s,s' = <a, b, c, s, t4> in let lab,lbc,lca,s1,s2 = t* in a I lab ∧ b I lab ∧ b I lbc ∧ c I lbc ∧ c I lca ∧ a\000C I lca ∈ ℙ
BY
{ (UnfoldpGeoAbbreviations (-1) THEN FoldpGeoAbbreviations (-1) THEN RepeatFor 4 (D -1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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
11.  t*  :  pgeo-triangle(pg*)
\mvdash{}  let  a,b,c,s,s'  =  <a,  b,  c,  s,  t4>  in  let  lab,lbc,lca,s1,s2  =  t*  in  a  I  lab
    \mwedge{}  b  I  lab
    \mwedge{}  b  I  lbc
    \mwedge{}  c  I  lbc
    \mwedge{}  c  I  lca
    \mwedge{}  a  I  lca  \mmember{}  \mBbbP{}


By

---

Latex:
(UnfoldpGeoAbbreviations  (-1)
  THEN  FoldpGeoAbbreviations  (-1)
  THEN  RepeatFor  4  (D  -1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index