---

Step * of Lemma opp-side_half-plane-angle-congruence

∀e:EuclideanPlane. ∀b,p,b',p',a,c,a',c':Point.
  ((a leftof bp ∧ c leftof pb) ⇒ (a' leftof b'p' ∧ c' leftof p'b') ⇒ (abp ≅a a'b'p' ∧ pbc ≅a p'b'c') ⇒ abc ≅a a'b'c')
BY
{ ((Auto
    THEN Duplicate (14)
    THEN Duplicate (15)
    ⋅)
   THEN ((D -1 THEN D 16) THEN ExRepD)
   THEN Unfold `geo-cong-angle` 0
   THEN GenRepD) }

1
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. a # b
17. b # p
18. a' # b'
19. b' # p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. p # b
32. b # c
33. p' # b'
34. b' # c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
⊢ ∃a'@0,c'@0,x',z':Point
   (B(baa'@0) ∧ B(bcc'@0) ∧ B(b'a'x') ∧ B(b'c'z') ∧ ba'@0 ≅ b'x' ∧ bc'@0 ≅ b'z' ∧ a'@0c'@0 ≅ x'z')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}b,p,b',p',a,c,a',c':Point.
    ((a  leftof  bp  \mwedge{}  c  leftof  pb)
    {}\mRightarrow{}  (a'  leftof  b'p'  \mwedge{}  c'  leftof  p'b')
    {}\mRightarrow{}  (abp  \mcong{}\msuba{}  a'b'p'  \mwedge{}  pbc  \mcong{}\msuba{}  p'b'c')
    {}\mRightarrow{}  abc  \mcong{}\msuba{}  a'b'c')


By

---

Latex:
((Auto
    THEN  Duplicate  (14)
    THEN  Duplicate  (15)
    \mcdot{})
  THEN  ((D  -1  THEN  D  16)  THEN  ExRepD)
  THEN  Unfold  `geo-cong-angle`  0
  THEN  GenRepD)

---

Home Index