---

Step * 1 4 of Lemma pgeo-minimum-order-proof2


1. pg : ProjectivePlane
2. n : ℕ
3. l : Line
4. p,q:{p:Point| p I l} //p ≡ q ~ ℕn + 1
5. ¬(n ≥ 2 )
6. a : Point
7. b : Point
8. c : Point
9. a I l
10. b I l
11. c I l
12. a ≠ b
13. b ≠ c
14. c ≠ a
15. {p:Point| p I l}  ⊆r (p,q:{p:Point| p I l} //p ≡ q)
16. (a ∈ {p:Point| p I l} ) ∧ (b ∈ {p:Point| p I l} ) ∧ (c ∈ {p:Point| p I l} )
17. ||[a; b; c]|| ≤ 2
⊢ n ≥ 2 
BY
{ (Reduce -1 THEN Auto) }

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlane
2.  n  :  \mBbbN{}
3.  l  :  Line
4.  p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q  \msim{}  \mBbbN{}n  +  1
5.  \mneg{}(n  \mgeq{}  2  )
6.  a  :  Point
7.  b  :  Point
8.  c  :  Point
9.  a  I  l
10.  b  I  l
11.  c  I  l
12.  a  \mneq{}  b
13.  b  \mneq{}  c
14.  c  \mneq{}  a
15.  \{p:Point|  p  I  l\}    \msubseteq{}r  (p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q)
16.  (a  \mmember{}  \{p:Point|  p  I  l\}  )  \mwedge{}  (b  \mmember{}  \{p:Point|  p  I  l\}  )  \mwedge{}  (c  \mmember{}  \{p:Point|  p  I  l\}  )
17.  ||[a;  b;  c]||  \mleq{}  2
\mvdash{}  n  \mgeq{}  2 


By

---

Latex:
(Reduce  -1  THEN  Auto)

---

Home Index