---

Step * 1 1 1 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
⊢ ¬¬(A=P=C ∧ B=P=D)
BY
{ Assert ⌜P' ≡ P⌝⋅ }

1
.....assertion..... 
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
⊢ P' ≡ P

2
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. P' ≡ P
⊢ ¬¬(A=P=C ∧ B=P=D)

---

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
\mvdash{}  \mneg{}\mneg{}(A=P=C  \mwedge{}  B=P=D)


By

---

Latex:
Assert  \mkleeneopen{}P'  \mequiv{}  P\mkleeneclose{}\mcdot{}

---

Home Index