Step * of Lemma pgeo-order-implies2

pg:ProjectivePlane. ∀n:ℕ.  (order(pg)  (∃l:Line. p,q:{p:Point| l} //p ≡ ~ ℕ1))
BY
((Auto THEN Unfold `pgeo-order` -1)
   THEN (InstLemma `pgeo-non-trivial-dual` [⌜pg⌝]⋅ THENA Auto)
   THEN -1
   THEN (InstConcl [⌜l⌝]⋅ THENA Auto)
   THEN InstHyp [⌜l⌝(3)⋅
   THEN Auto) }


Latex:


Latex:
\mforall{}pg:ProjectivePlane.  \mforall{}n:\mBbbN{}.    (order(pg)  =  n  {}\mRightarrow{}  (\mexists{}l:Line.  p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q  \msim{}  \mBbbN{}n  +  1))


By


Latex:
((Auto  THEN  Unfold  `pgeo-order`  -1)
  THEN  (InstLemma  `pgeo-non-trivial-dual`  [\mkleeneopen{}pg\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (InstConcl  [\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}l\mkleeneclose{}]  (3)\mcdot{}
  THEN  Auto)




Home Index