---

Step * 1 1 1 1 1 1 1 3 of Lemma implies-geo-between_functionality

.....antecedent..... 
1. e : EuclideanPlaneStructure
2. ∀a,b:Point.  (a # b ⇒ b # a)
3. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
4. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
5. ∀a,b,c:Point.  bc ≥ aa
6. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
7. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
8. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
9. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
10. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
11. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
12. ∀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)
13. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
14. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
15. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
16. ∀a,b1,b2,c:Point.  (b1 ≡ b2 ⇒ B(ab1c) ⇒ B(ab2c))
17. ∀a1,a2,b,c:Point.  (a1 ≡ a2 ⇒ B(a1bc) ⇒ B(a2bc))
18. ∀a:Point. a ≡ a
19. ∀a,b:Point.  ab ≅ ba
20. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
21. ∀a,b:Point.  (a # b ⇒ b # a)
22. ∀x,y:Point.  (x ≡ y ⇒ y ≡ x)
23. ∀x:Point. x ≡ x
24. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
25. a : Point
26. b : Point
27. c1 : Point
28. c2 : Point
29. c1 ≡ c2
30. B(abc1)
31. ∀a,b,x,y:Point.  ((¬ab>aa) ⇒ a leftof xy ⇒ b leftof xy)
32. ∀a,b,c,d,e1,f:Point.  (ab ≥ cd ⇒ cd ≥ e1f ⇒ ab ≥ e1f)
33. bc2>bc1
34. ∀a,b,c,d:Point.  (ab>cd ⇒ ba>cd)
⊢ bc1 ≥ bc2
BY
{ (D 0 THEN Auto) }

1
1. e : EuclideanPlaneStructure
2. ∀a,b:Point.  (a # b ⇒ b # a)
3. ∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)
4. ∀a,b,c:Point.  (ba>ac ⇒ b # c)
5. ∀a,b,c:Point.  bc ≥ aa
6. ∀a,b,c,d,e@0,f:Point.  (ab>cd ⇒ cd ≥ e@0f ⇒ ab>e@0f)
7. ∀a,b,c,d,e@0,f:Point.  (ab ≥ cd ⇒ cd>e@0f ⇒ ab>e@0f)
8. ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
9. ∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca)
10. ∀a,b,c:Point.  (a leftof bc ⇒ b # c)
11. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
12. ∀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)
13. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
14. ∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab)
15. ∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
16. ∀a,b1,b2,c:Point.  (b1 ≡ b2 ⇒ B(ab1c) ⇒ B(ab2c))
17. ∀a1,a2,b,c:Point.  (a1 ≡ a2 ⇒ B(a1bc) ⇒ B(a2bc))
18. ∀a:Point. a ≡ a
19. ∀a,b:Point.  ab ≅ ba
20. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
21. ∀a,b:Point.  (a # b ⇒ b # a)
22. ∀x,y:Point.  (x ≡ y ⇒ y ≡ x)
23. ∀x:Point. x ≡ x
24. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
25. a : Point
26. b : Point
27. c1 : Point
28. c2 : Point
29. c1 ≡ c2
30. B(abc1)
31. ∀a,b,x,y:Point.  ((¬ab>aa) ⇒ a leftof xy ⇒ b leftof xy)
32. ∀a,b,c,d,e1,f:Point.  (ab ≥ cd ⇒ cd ≥ e1f ⇒ ab ≥ e1f)
33. bc2>bc1
34. ∀a,b,c,d:Point.  (ab>cd ⇒ ba>cd)
35. bc2>bc1
⊢ False

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlaneStructure
2.  \mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)
3.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ab  \mgeq{}  cd)
4.  \mforall{}a,b,c:Point.    (ba>ac  {}\mRightarrow{}  b  \#  c)
5.  \mforall{}a,b,c:Point.    bc  \mgeq{}  aa
6.  \mforall{}a,b,c,d,e@0,f:Point.    (ab>cd  {}\mRightarrow{}  cd  \mgeq{}  e@0f  {}\mRightarrow{}  ab>e@0f)
7.  \mforall{}a,b,c,d,e@0,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd>e@0f  {}\mRightarrow{}  ab>e@0f)
8.  \mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  ac>ab)
9.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca)
10.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \#  c)
11.  \mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))
12.  \mforall{}a,b,c,d,A,B,C,D:Point.
            (a  \#  b  {}\mRightarrow{}  B(abc)  {}\mRightarrow{}  B(ABC)  {}\mRightarrow{}  ab  \mcong{}  AB  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  ad  \mcong{}  AD  {}\mRightarrow{}  bd  \mcong{}  BD  {}\mRightarrow{}  cd  \mcong{}  CD)
13.  \mforall{}a,b,c,x,y:Point.    (ax  \mcong{}  ay  {}\mRightarrow{}  bx  \mcong{}  by  {}\mRightarrow{}  cx  \mcong{}  cy  {}\mRightarrow{}  x  \#  y  {}\mRightarrow{}  (\mneg{}a  \#  bc))
14.  \mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  leftof  ab)
15.  \mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \#  b  {}\mRightarrow{}  (\mneg{}y  \#  ab)  {}\mRightarrow{}  y  \#  bc)
16.  \mforall{}a,b1,b2,c:Point.    (b1  \mequiv{}  b2  {}\mRightarrow{}  B(ab1c)  {}\mRightarrow{}  B(ab2c))
17.  \mforall{}a1,a2,b,c:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  B(a1bc)  {}\mRightarrow{}  B(a2bc))
18.  \mforall{}a:Point.  a  \mequiv{}  a
19.  \mforall{}a,b:Point.    ab  \mcong{}  ba
20.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
21.  \mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)
22.  \mforall{}x,y:Point.    (x  \mequiv{}  y  {}\mRightarrow{}  y  \mequiv{}  x)
23.  \mforall{}x:Point.  x  \mequiv{}  x
24.  \mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))
25.  a  :  Point
26.  b  :  Point
27.  c1  :  Point
28.  c2  :  Point
29.  c1  \mequiv{}  c2
30.  B(abc1)
31.  \mforall{}a,b,x,y:Point.    ((\mneg{}ab>aa)  {}\mRightarrow{}  a  leftof  xy  {}\mRightarrow{}  b  leftof  xy)
32.  \mforall{}a,b,c,d,e1,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd  \mgeq{}  e1f  {}\mRightarrow{}  ab  \mgeq{}  e1f)
33.  bc2>bc1
34.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ba>cd)
\mvdash{}  bc1  \mgeq{}  bc2


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index