---

Step * 1 3 1 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
⊢ <a ∨ b, b ∨ c, c ∨ a, s4, s5> ∈ pgeo-triangle(pg*)
BY
{ ((UnfoldpGeoAbbreviations (-1) THEN FoldpGeoAbbreviations (-1))
   THEN UnfoldpGeoAbbreviations 0
   THEN FoldpGeoAbbreviations 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
\mvdash{}  <a  \mvee{}  b,  b  \mvee{}  c,  c  \mvee{}  a,  s4,  s5>  \mmember{}  pgeo-triangle(pg*)


By

---

Latex:
((UnfoldpGeoAbbreviations  (-1)  THEN  FoldpGeoAbbreviations  (-1))
  THEN  UnfoldpGeoAbbreviations  0
  THEN  FoldpGeoAbbreviations  0
  THEN  Auto)

---

Home Index