---

Step * 1 1 1 of Lemma dual-plane_wf

.....equality..... 
1. pg : ProjectivePlaneStructureComplete
2. BasicProjectiveGeometryAxioms(pg)
3. triangle-axiom1(pg)
4. triangle-axiom2(pg)
⊢ let p,_ = pg "non-trivial" 
  in let l,_ = pg "three-lines" p 
     in l ~ TERMOF{pgeo-non-trivial-dual-ext:o, \\v:l, i:l} pg
BY
{ RepeatFor 2 ((Computation THEN Auto)) }

---

Latex:

---

Latex:
.....equality..... 
1.  pg  :  ProjectivePlaneStructureComplete
2.  BasicProjectiveGeometryAxioms(pg)
3.  triangle-axiom1(pg)
4.  triangle-axiom2(pg)
\mvdash{}  let  p,$_{}$  =  pg  "non-trivial" 
    in  let  l,$_{}$  =  pg  "three-lines"  p 
          in  l  \msim{}  TERMOF\{pgeo-non-trivial-dual-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  pg


By

---

Latex:
RepeatFor  2  ((Computation  THEN  Auto))

---

Home Index