Step
*
of Lemma
pgeo-non-trivial-dual-ext
∀g:ProjectivePlane. (∃l:Line [l ≡ l])
BY
{ Extract of Obid: pgeo-non-trivial-dual
  not unfolding  
  finishing with Auto
  normalizes to:
  
  λg.let p,_ = g "non-trivial" 
     in fst((g "three-lines" p)) }
Latex:
Latex:
\mforall{}g:ProjectivePlane.  (\mexists{}l:Line  [l  \mequiv{}  l])
By
Latex:
Extract  of  Obid:  pgeo-non-trivial-dual
not  unfolding   
finishing  with  Auto
normalizes  to:
\mlambda{}g.let  p,$_{}$  =  g  "non-trivial" 
      in  fst((g  "three-lines"  p))
Home
Index