Step
*
of Lemma
pgeo-order-implies2
∀pg:ProjectivePlane. ∀n:ℕ.  (order(pg) = n 
⇒ (∃l:Line. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1))
BY
{ ((Auto THEN Unfold `pgeo-order` -1)
   THEN (InstLemma `pgeo-non-trivial-dual` [⌜pg⌝]⋅ THENA Auto)
   THEN D -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