---

Step * of Lemma pgeo-triangle-dual

∀pg:ProjectivePlane. ∀t:pgeo-triangle(pg).
  ∃t*:pgeo-triangle(pg*)
   let a,b,c,s,s' = t 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 I lca
BY
{ (Auto THEN RepeatFor 4 (D -1)) }

1
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

---

Latex:

---

Latex:
\mforall{}pg:ProjectivePlane.  \mforall{}t:pgeo-triangle(pg).
    \mexists{}t*:pgeo-triangle(pg*)
      let  a,b,c,s,s'  =  t  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:
(Auto  THEN  RepeatFor  4  (D  -1))

---

Home Index