---

Step * 1 1 1 of Lemma basic-geo-sep-sym


1. e : GeometryPrimitives
2. BasicGeometryAxioms(e)
3. a : Point
4. b : Point
5. ab>aa
6. ∀a,b,c,d,x,y:Point.  (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
7. ∀a:Point. (¬a # a)
8. ∀a,b:Point.  ba ≥ ab
9. aa # bb)
⊢ False
BY
{ ((D 2 THEN SplitAndHyps) THEN D -1) }

1
1. e : GeometryPrimitives
2. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
3. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
4. ∀a,b,c:Point.  bc ≥ aa
5. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
7. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
8. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
9. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
10. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
11. ∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
12. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
13. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
14. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
15. a : Point
16. b : Point
17. ab>aa
18. ∀a,b,c,d,x,y:Point.  (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
19. ∀a:Point. (¬a # a)
20. ∀a,b:Point.  ba ≥ ab
21. bb>aa
⊢ False

2
1. e : GeometryPrimitives
2. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
3. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
4. ∀a,b,c:Point.  bc ≥ aa
5. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
6. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
7. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
8. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
9. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
10. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
11. ∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
12. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
13. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
14. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
15. a : Point
16. b : Point
17. ab>aa
18. ∀a,b,c,d,x,y:Point.  (ab ≅ cd ⇒ cd>xy ⇒ ab>xy)
19. ∀a:Point. (¬a # a)
20. ∀a,b:Point.  ba ≥ ab
21. aa>bb
⊢ False

---

Latex:

---

Latex:

1.  e  :  GeometryPrimitives
2.  BasicGeometryAxioms(e)
3.  a  :  Point
4.  b  :  Point
5.  ab>aa
6.  \mforall{}a,b,c,d,x,y:Point.    (ab  \mcong{}  cd  {}\mRightarrow{}  cd>xy  {}\mRightarrow{}  ab>xy)
7.  \mforall{}a:Point.  (\mneg{}a  \#  a)
8.  \mforall{}a,b:Point.    ba  \mgeq{}  ab
9.  aa  \#  bb)
\mvdash{}  False


By

---

Latex:
((D  2  THEN  SplitAndHyps)  THEN  D  -1)

---

Home Index