---

Step * of Lemma geo-lt-angle-trans

No Annotations
∀g:EuclideanPlane. ∀a,b,c,d,e,f,x,y,z:Point.  (abc < def ⇒ def < xyz ⇒ a # bc ⇒ d # ef ⇒ x # yz ⇒ abc < xyz)
BY
{ (Auto THEN (Unfold `geo-lt-angle` 11 THEN Unfold `geo-lt-angle` 12 THEN Unfold `geo-lt-angle` 0) THEN ExRepD) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
⊢ (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z'))

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f,x,y,z:Point.
    (abc  <  def  {}\mRightarrow{}  def  <  xyz  {}\mRightarrow{}  a  \#  bc  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  x  \#  yz  {}\mRightarrow{}  abc  <  xyz)


By

---

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

---

Home Index