---

Step * of Lemma geo-lt-angle_functionality

∀e:EuclideanPlane. ∀a,a',b,b',c,c',x,x',y,y',z,z':Point.
  (a ≡ a' ⇒ b ≡ b' ⇒ c ≡ c' ⇒ x ≡ x' ⇒ y ≡ y' ⇒ z ≡ z' ⇒ (abc < xyz ⇐⇒ a'b'c' < x'y'z'))
BY
{ (Auto THEN Unfold `geo-lt-angle` 0 THEN Unfold `geo-lt-angle` -1 THEN ExRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. a' : Point
4. b : Point
5. b' : Point
6. c : Point
7. c' : Point
8. x : Point
9. x' : Point
10. y : Point
11. y' : Point
12. z : Point
13. z' : Point
14. a ≡ a'
15. b ≡ b'
16. c ≡ c'
17. x ≡ x'
18. y ≡ y'
19. z ≡ z'
20. ¬out(y xz)
21. p : Point
22. p' : Point
23. x1 : Point
24. z1 : Point
25. abc ≅a xyp
26. y_p'_p
27. out(y xx1)
28. out(y zz1)
29. ¬x_y_p
30. x1_p'_z1
31. p' ≠ z1
⊢ (¬out(y' x'z'))
∧ (∃p,p',x'@0,z'@0:Point
    (a'b'c' ≅a x'y'p ∧ y'_p'_p ∧ (out(y' x'x'@0) ∧ out(y' z'z'@0)) ∧ (¬x'_y'_p) ∧ x'@0_p'_z'@0 ∧ p' ≠ z'@0))

2
1. e : EuclideanPlane
2. a : Point
3. a' : Point
4. b : Point
5. b' : Point
6. c : Point
7. c' : Point
8. x : Point
9. x' : Point
10. y : Point
11. y' : Point
12. z : Point
13. z' : Point
14. a ≡ a'
15. b ≡ b'
16. c ≡ c'
17. x ≡ x'
18. y ≡ y'
19. z ≡ z'
20. ¬out(y' x'z')
21. p : Point
22. p' : Point
23. x'@0 : Point
24. z'@0 : Point
25. a'b'c' ≅a x'y'p
26. y'_p'_p
27. out(y' x'x'@0)
28. out(y' z'z'@0)
29. ¬x'_y'_p
30. x'@0_p'_z'@0
31. p' ≠ z'@0
⊢ (¬out(y xz)) ∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ y_p'_p ∧ (out(y xx') ∧ out(y zz')) ∧ (¬x_y_p) ∧ x'_p'_z' ∧ p' ≠ z'))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,a',b,b',c,c',x,x',y,y',z,z':Point.
    (a  \mequiv{}  a'  {}\mRightarrow{}  b  \mequiv{}  b'  {}\mRightarrow{}  c  \mequiv{}  c'  {}\mRightarrow{}  x  \mequiv{}  x'  {}\mRightarrow{}  y  \mequiv{}  y'  {}\mRightarrow{}  z  \mequiv{}  z'  {}\mRightarrow{}  (abc  <  xyz  \mLeftarrow{}{}\mRightarrow{}  a'b'c'  <  x'y'z'))


By

---

Latex:
(Auto  THEN  Unfold  `geo-lt-angle`  0  THEN  Unfold  `geo-lt-angle`  -1  THEN  ExRepD)

---

Home Index