---

Step * 1 3 2 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} 
17. b ∈ {p:Point| p I l} 
18. c ∈ {p:Point| p I l} 
19. no_repeats(p,q:{p:Point| p I l} //p ≡ q;[b; c])
20. (a ∈ [c])
⊢ False
BY
{ (GenListD (-1) THEN EqTypeHD (-1) THEN Auto) }

1
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} 
17. b ∈ {p:Point| p I l} 
18. c ∈ {p:Point| p I l} 
19. no_repeats(p,q:{p:Point| p I l} //p ≡ q;[b; c])
20. a = c ∈ pertype(λp,q. ((p ∈ {p:Point| p I l} ) ∧ (q ∈ {p:Point| p I l} ) ∧ p ≡ q))
21. a ∈ {p:Point| p I l} 
22. c ∈ {p:Point| p I l} 
23. a ≡ c
⊢ False

---

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\} 
17.  b  \mmember{}  \{p:Point|  p  I  l\} 
18.  c  \mmember{}  \{p:Point|  p  I  l\} 
19.  no\_repeats(p,q:\{p:Point|  p  I  l\}  //p  \mequiv{}  q;[b;  c])
20.  (a  \mmember{}  [c])
\mvdash{}  False


By

---

Latex:
(GenListD  (-1)  THEN  EqTypeHD  (-1)  THEN  Auto)

---

Home Index