---

Step * 1 1 1 1 2 of Lemma opposite-side-congruent-diagonals-midpoint


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. P : Point
7. ¬Colinear(A;B;C)
8. B # D
9. AB ≅ CD
10. BC ≅ DA
11. Colinear(A;P;C)
12. Colinear(B;P;D)
13. P' : Point
14. BP ≅ DP'
15. PD ≅ P'B
16. DB ≅ BD
17. Colinear(D;P';B)
18. FSC(B;D;P;A  D;B;P';C)
19. FSC(B;D;P;C  D;B;P';A)
20. PA ≅ P'C
21. PC ≅ P'A
22. Colinear(A;P';C)
⊢ P' ≡ P
BY
{ (InstLemma `geo-intersection-unicity` [⌜e⌝;⌜A⌝;⌜C⌝;⌜B⌝;⌜D⌝;⌜P⌝;⌜P'⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  P  :  Point
7.  \mneg{}Colinear(A;B;C)
8.  B  \#  D
9.  AB  \mcong{}  CD
10.  BC  \mcong{}  DA
11.  Colinear(A;P;C)
12.  Colinear(B;P;D)
13.  P'  :  Point
14.  BP  \mcong{}  DP'
15.  PD  \mcong{}  P'B
16.  DB  \mcong{}  BD
17.  Colinear(D;P';B)
18.  FSC(B;D;P;A    D;B;P';C)
19.  FSC(B;D;P;C    D;B;P';A)
20.  PA  \mcong{}  P'C
21.  PC  \mcong{}  P'A
22.  Colinear(A;P';C)
\mvdash{}  P'  \mequiv{}  P


By

---

Latex:
(InstLemma  `geo-intersection-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index