---

Step * 1 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;[c])
⊢ ¬(b ∈ [c])
BY
{ ((D 0 THENA Auto) THEN GenListD (-1)) }

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;[c])
20. b = c ∈ (p,q:{p:Point| p I l} //p ≡ q)
⊢ 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;[c])
\mvdash{}  \mneg{}(b  \mmember{}  [c])


By

---

Latex:
((D  0  THENA  Auto)  THEN  GenListD  (-1))

---

Home Index