---

Step * 1 1 1 1 1 of Lemma cong3-in-half-plane


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. u : Point
8. c # ab
9. u # xy
10. ab ≅ xy
11. p : Point
12. Colinear(a;b;p)
13. ab  ⊥p pc
14. q : Point
15. Colinear(x;y;q)
16. Cong3(abp,xyq)
17. r : Point
18. l : Point
19. xy  ⊥q lq
20. xy  ⊥q rq
21. l leftof xy
22. r leftof yx
23. r # l
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy ⇐⇒ z leftof xy))
BY
{ ((Assert r # q BY
          ((Assert r # yx BY Auto) THEN (RWO "lsep-iff-all-sep" (-1) THENA Auto) THEN Auto))
   THEN (Assert l # q BY
               ((Assert l # xy BY Auto) THEN (RWO "lsep-iff-all-sep" (-1) THENA Auto) THEN Auto))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. u : Point
8. c # ab
9. u # xy
10. ab ≅ xy
11. p : Point
12. Colinear(a;b;p)
13. ab  ⊥p pc
14. q : Point
15. Colinear(x;y;q)
16. Cong3(abp,xyq)
17. r : Point
18. l : Point
19. xy  ⊥q lq
20. xy  ⊥q rq
21. l leftof xy
22. r leftof yx
23. r # l
24. r # q
25. l # q
⊢ ∃z:Point. (Cong3(abc,xyz) ∧ z # xy ∧ (u leftof xy ⇐⇒ z leftof xy))

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  u  :  Point
8.  c  \#  ab
9.  u  \#  xy
10.  ab  \mcong{}  xy
11.  p  :  Point
12.  Colinear(a;b;p)
13.  ab    \mbot{}p  pc
14.  q  :  Point
15.  Colinear(x;y;q)
16.  Cong3(abp,xyq)
17.  r  :  Point
18.  l  :  Point
19.  xy    \mbot{}q  lq
20.  xy    \mbot{}q  rq
21.  l  leftof  xy
22.  r  leftof  yx
23.  r  \#  l
\mvdash{}  \mexists{}z:Point.  (Cong3(abc,xyz)  \mwedge{}  z  \#  xy  \mwedge{}  (u  leftof  xy  \mLeftarrow{}{}\mRightarrow{}  z  leftof  xy))


By

---

Latex:
((Assert  r  \#  q  BY
                ((Assert  r  \#  yx  BY  Auto)  THEN  (RWO  "lsep-iff-all-sep"  (-1)  THENA  Auto)  THEN  Auto))
  THEN  (Assert  l  \#  q  BY
                          ((Assert  l  \#  xy  BY  Auto)  THEN  (RWO  "lsep-iff-all-sep"  (-1)  THENA  Auto)  THEN  Auto))
  )

---

Home Index