---

Step * 1 1 of Lemma dual-plane_wf


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 ∈ Line
BY
{ Subst' 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 0 }

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

2
1. pg : ProjectivePlaneStructureComplete
2. BasicProjectiveGeometryAxioms(pg)
3. triangle-axiom1(pg)
4. triangle-axiom2(pg)
⊢ TERMOF{pgeo-non-trivial-dual-ext:o, \\v:l, i:l} pg ∈ Line

---

Latex:

---

Latex:

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  \mmember{}  Line


By

---

Latex:
Subst'  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  0

---

Home Index