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,_ "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