---

Step * 1 of Lemma interior-point-preserves-cong-angle


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. abc ≅a xyz
11. a_q_c
12. x_p_z
13. Cong3(abc,xyz)
14. Cong3(aqc,xpz)
15. x # yz
16. qb ≅ py
⊢ ((a ≠ b ∧ b ≠ q) ∧ x ≠ y) ∧ y ≠ p
BY
{ ((InstLemma `geo-sep-or` [⌜g⌝;⌜x⌝;⌜z⌝;⌜p⌝]⋅ THENA Auto) THEN D -1) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. abc ≅a xyz
11. a_q_c
12. x_p_z
13. Cong3(abc,xyz)
14. Cong3(aqc,xpz)
15. x # yz
16. qb ≅ py
17. x ≠ p
⊢ ((a ≠ b ∧ b ≠ q) ∧ x ≠ y) ∧ y ≠ p

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. abc ≅a xyz
11. a_q_c
12. x_p_z
13. Cong3(abc,xyz)
14. Cong3(aqc,xpz)
15. x # yz
16. qb ≅ py
17. z ≠ p
⊢ ((a ≠ b ∧ b ≠ q) ∧ x ≠ y) ∧ y ≠ p

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  p  :  Point
9.  q  :  Point
10.  abc  \mcong{}\msuba{}  xyz
11.  a\_q\_c
12.  x\_p\_z
13.  Cong3(abc,xyz)
14.  Cong3(aqc,xpz)
15.  x  \#  yz
16.  qb  \mcong{}  py
\mvdash{}  ((a  \mneq{}  b  \mwedge{}  b  \mneq{}  q)  \mwedge{}  x  \mneq{}  y)  \mwedge{}  y  \mneq{}  p


By

---

Latex:
((InstLemma  `geo-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index