---

Step * 1 of Lemma congruent-half-plane-angles-implies-right-angles


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a # cd
8. abc ≅a abd
9. a ≠ b
10. Rabc ⇐⇒ abc ≅a abd
⊢ {Rabd ∧ Rabc}
BY
{ ((Assert abd ≅a abc BY
          EAuto 1)
   THEN (RepeatFor 2 (D -2) THEN Auto)
   THEN (InstLemma `adjacent-right-angles-supplementary` [⌜g⌝;⌜a⌝;⌜b⌝;⌜d⌝;⌜c⌝]⋅ THENA Auto)
   THEN (RepeatFor 2 (D -1) THEN Auto)
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  c-b-d
7.  a  \#  cd
8.  abc  \mcong{}\msuba{}  abd
9.  a  \mneq{}  b
10.  Rabc  \mLeftarrow{}{}\mRightarrow{}  abc  \mcong{}\msuba{}  abd
\mvdash{}  \{Rabd  \mwedge{}  Rabc\}


By

---

Latex:
((Assert  abd  \mcong{}\msuba{}  abc  BY
                EAuto  1)
  THEN  (RepeatFor  2  (D  -2)  THEN  Auto)
  THEN  (InstLemma  `adjacent-right-angles-supplementary`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (D  -1)  THEN  Auto)
  THEN  D  0
  THEN  Auto)

---

Home Index