---

Step * 2 2 1 of Lemma perp-in-congruence


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. A : Point
5. B : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. ab ≅ AB
11. ac ≅ AC
12. bc ≅ BC
13. AB  ⊥D DC
14. ab  ⊥d dc
15. a ≠ b
16. ad ≅ AD
17. bd ≅ BD
18. ad ≅ AD
19. bd ≅ BD
⊢ cd ≅ CD
BY
{ (All (Unfold `geo-perp-in`) THEN EasyGeometry) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  A  :  Point
5.  B  :  Point
6.  c  :  Point
7.  d  :  Point
8.  C  :  Point
9.  D  :  Point
10.  ab  \mcong{}  AB
11.  ac  \mcong{}  AC
12.  bc  \mcong{}  BC
13.  AB    \mbot{}D  DC
14.  ab    \mbot{}d  dc
15.  a  \mneq{}  b
16.  ad  \mcong{}  AD
17.  bd  \mcong{}  BD
18.  ad  \mcong{}  AD
19.  bd  \mcong{}  BD
\mvdash{}  cd  \mcong{}  CD


By

---

Latex:
(All  (Unfold  `geo-perp-in`)  THEN  EasyGeometry)

---

Home Index