---

Step * 1 2 of Lemma pgeo-triangle-dual

.....assertion..... 
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
⊢ a ∨ b ≠ b ∨ c ∨ c ∨ a
BY
{ (UnfoldpGeoAbbreviations 0 THEN FoldpGeoAbbreviations 0 THEN Auto) }

1
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
⊢ b ∨ c ∧ c ∨ a ≠ a ∨ b

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  a  \mvee{}  b  \mneq{}  b  \mvee{}  c  \mvee{}  c  \mvee{}  a


By

---

Latex:
(UnfoldpGeoAbbreviations  0  THEN  FoldpGeoAbbreviations  0  THEN  Auto)

---

Home Index