---

Step * 1 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
⊢ ∃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\000C ∧ c I lbc ∧ c I lca ∧ a I lca
BY
{ ((Assert a ≠ b ∧ c ≠ a BY
          (FLemma `plsep-join-implies` [-1] THEN EAuto 1))
   THEN D -1
   THEN RenameVar `s2' (-2)
   THEN RenameVar `s3' (-1)
   THEN (Assert ⌜b ∨ c ≠ c ∨ a⌝⋅
   THENM (RenameVar `s4' (-1) THEN (Assert ⌜a ∨ b ≠ b ∨ c ∨ c ∨ a⌝⋅ THENM RenameVar `s5' (-1)))
   )) }

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

2
.....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

3
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
⊢ ∃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\000C ∧ c I lbc ∧ c I lca ∧ a I lca

---

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
\mvdash{}  \mexists{}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
      \mwedge{}  b  I  lab
      \mwedge{}  b  I  lbc
      \mwedge{}  c  I  lbc
      \mwedge{}  c  I  lca
      \mwedge{}  a  I  lca


By

---

Latex:
((Assert  a  \mneq{}  b  \mwedge{}  c  \mneq{}  a  BY
                (FLemma  `plsep-join-implies`  [-1]  THEN  EAuto  1))
  THEN  D  -1
  THEN  RenameVar  `s2'  (-2)
  THEN  RenameVar  `s3'  (-1)
  THEN  (Assert  \mkleeneopen{}b  \mvee{}  c  \mneq{}  c  \mvee{}  a\mkleeneclose{}\mcdot{}
  THENM  (RenameVar  `s4'  (-1)  THEN  (Assert  \mkleeneopen{}a  \mvee{}  b  \mneq{}  b  \mvee{}  c  \mvee{}  c  \mvee{}  a\mkleeneclose{}\mcdot{}  THENM  RenameVar  `s5'  (-1)))
  ))

---

Home Index