---

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


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. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. A : Point
21. a'-b'-A
22. b'A ≅ a'b'
23. a'' : Point
24. A-b'-a''
25. b'a'' ≅ ba
26. C : Point
27. c'-b'-C
28. b'C ≅ a'b'
29. c'' : Point
30. C-b'-c''
31. b'c'' ≅ bc
⊢ out(b' a'a'')
BY
{ ((D 24 THEN D 21) THEN InstLemma `geo-out-iff-between1` [⌜e⌝;⌜b'⌝;⌜a'⌝;⌜a''⌝;⌜A⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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.  d  :  Point
11.  a  leftof  bp
12.  c  leftof  pb
13.  a'  leftof  b'p'
14.  c'  leftof  p'b'
15.  abp  \mcong{}\msuba{}  a'b'p'
16.  pbc  \mcong{}\msuba{}  p'b'c'
17.  a-d-c
18.  out(b  dp)
19.  b  \mneq{}  d
20.  A  :  Point
21.  a'-b'-A
22.  b'A  \mcong{}  a'b'
23.  a''  :  Point
24.  A-b'-a''
25.  b'a''  \mcong{}  ba
26.  C  :  Point
27.  c'-b'-C
28.  b'C  \mcong{}  a'b'
29.  c''  :  Point
30.  C-b'-c''
31.  b'c''  \mcong{}  bc
\mvdash{}  out(b'  a'a'')


By

---

Latex:
((D  24  THEN  D  21)  THEN  InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}a''\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index