---

Step * 1 1 6 1 of Lemma euclidean-plane-axioms

.....aux..... 
1. g : EuclideanPlane
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,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef)
6. ∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef)
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,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
16. SqStable(geo-left-axioms(g))
17. ∀a:Point. a ≡ a
18. ∀a,b:Point.  ab ≅ ba
19. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
20. ∀a,b:Point.  (a # b ⇒ b # a)
21. a : Point
22. b : Point
23. p : Point
24. q : Point
25. r : Point
26. s : Point
27. ab ≅ pq
28. ab ≅ rs
29. a1 : Point
30. b1 : Point
31. c : Point
32. d : Point
33. x : Point
34. y : Point
35. a1b1 ≅ cd
36. cd>xy
37. ¬cd>a1b1
⊢ a1b1>xy
BY
{ (Unfold `geo-ge` 6
   THEN (InstHyp [⌜c⌝;⌜d⌝;⌜a1⌝;⌜b1⌝;⌜x⌝;⌜y⌝] (6)⋅ THEN Auto)
   THEN (D 0 THENA Auto)
   THEN D 35
   THEN Unfold `geo-length-sep` 0
   THEN OrRight
   THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  EuclideanPlane
2.  \mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ab  \mgeq{}  cd)
3.  \mforall{}a,b,c:Point.    (ba>ac  {}\mRightarrow{}  b  \#  c)
4.  \mforall{}a,b,c:Point.    bc  \mgeq{}  aa
5.  \mforall{}a,b,c,d,e,f:Point.    (ab>cd  {}\mRightarrow{}  cd  \mgeq{}  ef  {}\mRightarrow{}  ab>ef)
6.  \mforall{}a,b,c,d,e,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd>ef  {}\mRightarrow{}  ab>ef)
7.  \mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  ac>ab)
8.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  leftof  ca)
9.  \mforall{}a,b,c:Point.    (a  leftof  bc  {}\mRightarrow{}  b  \#  c)
10.  \mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))
11.  \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)
12.  \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))
13.  \mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  leftof  ab)
14.  \mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \#  b  {}\mRightarrow{}  (\mneg{}y  \#  ab)  {}\mRightarrow{}  y  \#  bc)
15.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c)))
16.  SqStable(geo-left-axioms(g))
17.  \mforall{}a:Point.  a  \mequiv{}  a
18.  \mforall{}a,b:Point.    ab  \mcong{}  ba
19.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
20.  \mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)
21.  a  :  Point
22.  b  :  Point
23.  p  :  Point
24.  q  :  Point
25.  r  :  Point
26.  s  :  Point
27.  ab  \mcong{}  pq
28.  ab  \mcong{}  rs
29.  a1  :  Point
30.  b1  :  Point
31.  c  :  Point
32.  d  :  Point
33.  x  :  Point
34.  y  :  Point
35.  a1b1  \mcong{}  cd
36.  cd>xy
37.  \mneg{}cd>a1b1
\mvdash{}  a1b1>xy


By

---

Latex:
(Unfold  `geo-ge`  6
  THEN  (InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (6)\mcdot{}  THEN  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  35
  THEN  Unfold  `geo-length-sep`  0
  THEN  OrRight
  THEN  Auto)

---

Home Index